:: Linear Combinations in Right Module over Associative Ring
::  by Michal Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, FUNCSDOM, VECTSP_2, VECTSP_1, FINSEQ_1, NAT_1, SUBSET_1,
      FUNCT_1, FINSET_1, ARYTM_3, RELAT_1, CARD_3, XXREAL_0, TARSKI, CARD_1,
      STRUCT_0, SUPINF_2, PARTFUN1, XBOOLE_0, ORDINAL4, ARYTM_1, RLVECT_2,
      FUNCT_2, FUNCOP_1, VALUED_1, GROUP_1, RLSUB_1, FINSEQ_4, RLVECT_3,
      RMOD_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, FINSET_1, FINSEQ_1, NUMBERS,
      RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, ORDINAL1, NAT_1, CARD_1, DOMAIN_1,
      STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, FINSEQ_4, FUNCSDOM,
      VECTSP_2, RMOD_2, RMOD_3, FUNCOP_1, XXREAL_0;
 constructors PARTFUN1, DOMAIN_1, FUNCOP_1, XXREAL_0, NAT_1, FINSEQ_4,
      RLVECT_2, RMOD_2, RMOD_3, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, XREAL_0,
      STRUCT_0, VECTSP_1, ORDINAL1, FINSEQ_1, VECTSP_2, RMOD_2, CARD_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET;
 definitions FUNCT_1, TARSKI, RMOD_2, XBOOLE_0, RELAT_1;
 theorems CARD_1, CARD_2, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4,
      FUNCT_1, FUNCT_2, RLVECT_1, RLVECT_2, TARSKI, VECTSP_1, VECTSP_2,
      ZFMISC_1, RMOD_2, NAT_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, RLSUB_2,
      XCMPLX_1, GROUP_1, FUNCOP_1, XREAL_1, PARTFUN1, STRUCT_0, RMOD_3;
 schemes FINSEQ_1, FUNCT_2, NAT_1;

begin

reserve R for Ring,
  V for RightMod of R,
  a,b for Scalar of R,
  x,y for set,
  p,q ,r for FinSequence,
  i,k for Nat,
  u,v,v1,v2,v3,w for Vector of V,
  F,G,H for FinSequence of V,
  A,B for Subset of V,
  f for Function of V, R,
  S,T for finite Subset of V;

Lm1: len F = len G + 1 & G = F | (Seg len G) & v = F.(len F) implies Sum(F) =
Sum(G) + v
proof
  len F = len G + 1 & G = F | (dom G) & v = F.(len F) implies Sum(F) = Sum
  (G) + v by RLVECT_1:38;
  hence thesis by FINSEQ_1:def 3;
end;

theorem Th1:
  len F = len G & (for k,v st k in dom F & v = G.k holds F.k = v *
  a) implies Sum(F) = Sum(G) * a
proof
  defpred P[Nat] means for H,I be FinSequence of V st len H = len I & len H =
$1 & (for k,v st k in dom H & v = I.k holds H.k = v * a) holds Sum(H) = Sum(I)
  * a;
  now
    let n be Element of NAT;
    assume
A1: for H,I be FinSequence of V st len H = len I & len H = n & for k,
    v st k in dom H & v = I.k holds H.k = v * a holds Sum(H) = Sum(I) * a;
    let H,I be FinSequence of V;
    assume that
A2: len H = len I and
A3: len H = n + 1 and
A4: for k,v st k in dom H & v = I.k holds H.k = v * a;
    reconsider p = H | (Seg n),q = I | (Seg n) as FinSequence of V by
FINSEQ_1:18;
A5: n <= n + 1 by NAT_1:12;
    then
A6: len p = n by A3,FINSEQ_1:17;
A7: len q = n by A2,A3,A5,FINSEQ_1:17;
A8: now
      len p <= len H by A3,A5,FINSEQ_1:17;
      then
A9:   dom p c= dom H by FINSEQ_3:30;
      let k,v;
      assume that
A10:  k in dom p and
A11:  v = q.k;
      dom p = dom q by A6,A7,FINSEQ_3:29;
      then I.k = q.k by A10,FUNCT_1:47;
      then H.k = v * a by A4,A10,A11,A9;
      hence p.k = v * a by A10,FUNCT_1:47;
    end;
A12: n + 1 in Seg(n + 1) by FINSEQ_1:4;
    then n + 1 in dom H & n + 1 in dom I by A2,A3,FINSEQ_1:def 3;
    then reconsider v1 = H.(n + 1),v2 = I.(n + 1) as Vector of V by FINSEQ_2:11
;
    n + 1 in dom H by A3,A12,FINSEQ_1:def 3;
    then
A13: v1 = v2 * a by A4;
    thus Sum(H) = Sum(p) + v1 by A3,A6,Lm1
      .= Sum(q) * a + v2 * a by A1,A6,A7,A8,A13
      .= (Sum(q) + v2) * a by VECTSP_2:def 9
      .= Sum(I) * a by A2,A3,A7,Lm1;
  end;
  then
A14: for i be Element of NAT st P[i] holds P[i+1];
  now
    let H,I be FinSequence of V;
    assume that
A15: len H = len I and
A16: len H = 0 and
    for k,v st k in dom H & v = I.k holds H.k = v * a;
    H = <*>(the carrier of V) by A16;
    then
A17: Sum(H) = 0.V by RLVECT_1:43;
    I = <*>(the carrier of V) by A15,A16;
    then Sum(I) = 0.V by RLVECT_1:43;
    hence Sum(H) = Sum(I) * a by A17,VECTSP_2:32;
  end;
  then
A18: P[0];
  for n being Element of NAT holds P[n] from NAT_1:sch 1(A18,A14);
  hence thesis;
end;

Lm2: len F = len G & (for k st k in dom F holds G.k = F/.k * a) implies Sum(G)
= Sum(F) * a
proof
  assume that
A1: len F = len G and
A2: for k st k in dom F holds G.k = F/.k * a;
  now
    let k,v;
    assume that
A3: k in dom G and
A4: v = F.k;
A5: k in dom F by A1,A3,FINSEQ_3:29;
    then v = F/.k by A4,PARTFUN1:def 6;
    hence G.k = v * a by A2,A5;
  end;
  hence thesis by A1,Th1;
end;

theorem
  Sum(<*>(the carrier of V)) * a = 0.V
proof
  thus Sum(<*>(the carrier of V)) * a = 0.V * a by RLVECT_1:43
    .= 0.V by VECTSP_2:32;
end;

theorem
  Sum<* v,u *> * a = v * a + u * a
proof
  thus Sum<* v,u *> * a = (v + u) * a by RLVECT_1:45
    .= v * a + u * a by VECTSP_2:def 9;
end;

theorem
  Sum<* v,u,w *> * a = v * a + u * a + w * a
proof
  thus Sum<* v,u,w *> * a = (v + u + w) * a by RLVECT_1:46
    .= (v + u) * a + w * a by VECTSP_2:def 9
    .= v * a + u * a + w * a by VECTSP_2:def 9;
end;

definition
  let R, V, T;

  func Sum(T) -> Vector of V means
  :Def1:
  ex F st rng F = T & F is one-to-one & it = Sum(F);
  existence
  proof
    consider p such that
A1: rng p = T and
A2: p is one-to-one by FINSEQ_4:58;
    reconsider p as FinSequence of V by A1,FINSEQ_1:def 4;
    take Sum(p);
    take p;
    thus thesis by A1,A2;
  end;
  uniqueness by RLVECT_1:42;
end;

theorem Th5:
  Sum({}V) = 0.V
proof
  Sum(<*>(the carrier of V)) = 0.V by RLVECT_1:43;
  hence thesis by Def1,RELAT_1:38;
end;

theorem
  Sum{v} = v
proof
A1: Sum<* v *> = v by RLVECT_1:44;
  rng<* v *> = {v} & <* v *> is one-to-one by FINSEQ_1:39,FINSEQ_3:93;
  hence thesis by A1,Def1;
end;

theorem
  v1 <> v2 implies Sum{v1,v2} = v1 + v2
proof
  assume v1 <> v2;
  then
A1: <* v1,v2 *> is one-to-one by FINSEQ_3:94;
  rng<* v1,v2 *> = {v1,v2} & Sum<* v1,v2 *> = v1 + v2 by FINSEQ_2:127
,RLVECT_1:45;
  hence thesis by A1,Def1;
end;

theorem
  v1 <> v2 & v2 <> v3 & v1 <> v3 implies Sum{v1,v2,v3} = v1 + v2 + v3
proof
  assume v1 <> v2 & v2 <> v3 & v1 <> v3;
  then
A1: <* v1,v2,v3 *> is one-to-one by FINSEQ_3:95;
  rng<* v1,v2,v3 *> = {v1,v2,v3} & Sum<* v1,v2,v3 *> = v1 + v2 + v3 by
FINSEQ_2:128,RLVECT_1:46;
  hence thesis by A1,Def1;
end;

theorem Th9:
  T misses S implies Sum(T \/ S) = Sum(T) + Sum(S)
proof
  consider F such that
A1: rng F = T \/ S and
A2: F is one-to-one & Sum(T \/ S) = Sum(F) by Def1;
  consider G such that
A3: rng G = T and
A4: G is one-to-one and
A5: Sum(T) = Sum(G) by Def1;
  consider H such that
A6: rng H = S and
A7: H is one-to-one and
A8: Sum(S) = Sum(H) by Def1;
  set I = G ^ H;
  assume T misses S;
  then
A9: I is one-to-one by A3,A4,A6,A7,FINSEQ_3:91;
  rng I = rng F by A1,A3,A6,FINSEQ_1:31;
  hence Sum(T \/ S) = Sum(I) by A2,A9,RLVECT_1:42
    .= Sum(T) + Sum(S) by A5,A8,RLVECT_1:41;
end;

theorem Th10:
  Sum(T \/ S) = Sum(T) + Sum(S) - Sum(T /\ S)
proof
  set A = S \ T;
  set B = T \ S;
  set Z = A \/ B;
  set I = T /\ S;
A1: A \/ I = S by XBOOLE_1:51;
A2: B \/ I = T by XBOOLE_1:51;
A3: Z = T \+\ S;
  then Z \/ I = T \/ S by XBOOLE_1:93;
  then Sum(T \/ S) + Sum(I) = Sum(Z) + Sum(I) + Sum(I) by A3,Th9,XBOOLE_1:103
    .= Sum(A) + Sum(B) + Sum(I) + Sum(I) by Th9,XBOOLE_1:82
    .= Sum(A) + (Sum(I) + Sum(B)) + Sum(I) by RLVECT_1:def 3
    .= (Sum(A) + Sum(I)) + (Sum(B) + Sum(I)) by RLVECT_1:def 3
    .= Sum(S) + (Sum(B) + Sum(I)) by A1,Th9,XBOOLE_1:89
    .= Sum(T) + Sum(S) by A2,Th9,XBOOLE_1:89;
  hence thesis by RLSUB_2:61;
end;

theorem
  Sum(T /\ S) = Sum(T) + Sum(S) - Sum(T \/ S)
proof
  Sum(T \/ S) = Sum(T) + Sum(S) - Sum(T /\ S) by Th10;
  then Sum(T) + Sum(S) = Sum(T /\ S) + Sum(T \/ S) by RLSUB_2:61;
  hence thesis by RLSUB_2:61;
end;

theorem Th12:
  Sum(T \ S) = Sum(T \/ S) - Sum(S)
proof
  (T \ S) misses S by XBOOLE_1:79;
  then
A1: (T \ S) /\ S = {}V by XBOOLE_0:def 7;
  (T \ S) \/ S = T \/ S by XBOOLE_1:39;
  then Sum(T \/ S) = Sum(T \ S) + Sum(S) - Sum((T \ S) /\ S) by Th10;
  then Sum(T \/ S) = Sum(T \ S) + Sum(S) - 0.V by A1,Th5
    .= Sum(T \ S) + Sum(S) by VECTSP_1:18;
  hence thesis by RLSUB_2:61;
end;

theorem Th13:
  Sum(T \ S) = Sum(T) - Sum(T /\ S)
proof
  T \ (T /\ S) = T \ S by XBOOLE_1:47;
  then Sum(T \ S) = Sum(T \/ (T /\ S)) - Sum(T /\ S) by Th12;
  hence thesis by XBOOLE_1:22;
end;

theorem
  Sum(T \+\ S) = Sum(T \/ S) - Sum(T /\ S)
proof
  T \+\ S = (T \/ S) \ (T /\ S) by XBOOLE_1:101;
  hence Sum(T \+\ S) = Sum(T \/ S) - Sum((T \/ S) /\ (T /\ S)) by Th13
    .= Sum(T \/ S) - Sum((T \/ S) /\ T /\ S) by XBOOLE_1:16
    .= Sum(T \/ S) - Sum(T /\ S) by XBOOLE_1:21;
end;

theorem
  Sum(T \+\ S) = Sum(T \ S) + Sum(S \ T) by Th9,XBOOLE_1:82;

definition
  let R, V;
  mode Linear_Combination of V -> Element of Funcs(the carrier of V, the
    carrier of R) means
    :Def2:
    ex T st for v st not v in T holds it.v = 0.R;
  existence
  proof
    {}V = {};
    then reconsider P = {} as finite Subset of V;
    reconsider f = (the carrier of V) --> 0.R as Function of V, R;
    reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
    take f;
    take P;
    thus thesis by FUNCOP_1:7;
  end;
end;

reserve L,L1,L2,L3 for Linear_Combination of V;

definition
  let R, V, L;
  func Carrier(L) -> finite Subset of V equals
  {v : L.v <> 0.R};
  coherence
  proof
    set A = {v : L.v <> 0.R};
    consider T such that
A1: for v st not v in T holds L.v = 0.R by Def2;
    A c= T
    proof
      let x;
      assume x in A;
      then ex v st x = v & L.v <> 0.R;
      hence thesis by A1;
    end;
    hence thesis by XBOOLE_1:1;
  end;
end;

theorem
  x in Carrier(L) iff ex v st x = v & L.v <> 0.R;

theorem
  L.v = 0.R iff not v in Carrier(L)
proof
  thus L.v = 0.R implies not v in Carrier(L)
  proof
    assume
A1: L.v = 0.R;
    assume not thesis;
    then ex u st u = v & L.u <> 0.R;
    hence thesis by A1;
  end;
  assume not v in Carrier(L);
  hence thesis;
end;

definition
  let R, V;
  func ZeroLC(V) -> Linear_Combination of V means
  :Def4:
  Carrier(it) = {};
  existence
  proof
    reconsider f = (the carrier of V) --> 0.R as Function of V, R;
    reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
    f is Linear_Combination of V
    proof
      reconsider T = {}V as finite empty Subset of V;
      take T;
      thus thesis by FUNCOP_1:7;
    end;
    then reconsider f as Linear_Combination of V;
    take f;
    set C = {v : f.v <> 0.R};
    now
      set x = the Element of C;
      assume C <> {};
      then x in C;
      then ex v st x = v & f.v <> 0.R;
      hence contradiction by FUNCOP_1:7;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let L,L9 be Linear_Combination of V;
    assume that
A1: Carrier(L) = {} and
A2: Carrier(L9) = {};
    now
      let x;
      assume x in the carrier of V;
      then reconsider v = x as Element of V;
A3:   now
        assume L9.v <> 0.R;
        then v in {u : L9.u <> 0.R};
        hence contradiction by A2;
      end;
      now
        assume L.v <> 0.R;
        then v in {u : L.u <> 0.R};
        hence contradiction by A1;
      end;
      hence L.x = L9.x by A3;
    end;
    hence L = L9 by FUNCT_2:12;
  end;
end;

theorem Th18:
  ZeroLC(V).v = 0.R
proof
  Carrier(ZeroLC(V)) = {} & not v in {} by Def4;
  hence thesis;
end;

definition
  let R, V, A;
  mode Linear_Combination of A -> Linear_Combination of V means
    :Def5:
    Carrier (it) c= A;
  existence
  proof
    take L = ZeroLC(V);
    Carrier(L) = {} by Def4;
    hence thesis by XBOOLE_1:2;
  end;
end;

reserve l for Linear_Combination of A;

theorem Th19:
  A c= B implies l is Linear_Combination of B
proof
  assume
A1: A c= B;
  Carrier(l) c= A by Def5;
  then Carrier(l) c= B by A1,XBOOLE_1:1;
  hence thesis by Def5;
end;

theorem Th20:
  ZeroLC(V) is Linear_Combination of A
proof
  Carrier(ZeroLC(V)) = {} & {} c= A by Def4,XBOOLE_1:2;
  hence thesis by Def5;
end;

theorem Th21:
  for l being Linear_Combination of {}(the carrier of V) holds l = ZeroLC(V)
proof
  let l be Linear_Combination of {}(the carrier of V);
  Carrier(l) c= {} by Def5;
  then Carrier(l) = {};
  hence thesis by Def4;
end;

theorem
  L is Linear_Combination of Carrier(L) by Def5;

definition
  let R, V, F, f;
  func f (#) F -> FinSequence of V means
  :Def6:
  len it = len F & for i being
  Nat st i in dom it holds it.i = (F/.i) * f.(F/.i);
  existence
  proof
    deffunc Q(Nat) = (F/.$1)*f.(F/.$1);
    consider G being FinSequence such that
A1: len G = len F and
A2: for n be Nat st n in dom G holds G.n = Q(n) from FINSEQ_1:sch 2;
    rng G c= the carrier of V
    proof
      let x;
      assume x in rng G;
      then consider y be set such that
A3:   y in dom G and
A4:   G.y = x by FUNCT_1:def 3;
      y in Seg(len F) by A1,A3,FINSEQ_1:def 3;
      then reconsider y as Element of NAT;
      G.y = (F/.y) * f.(F/.y) by A2,A3;
      hence thesis by A4;
    end;
    then reconsider G as FinSequence of V by FINSEQ_1:def 4;
    take G;
    thus thesis by A1,A2;
  end;
  uniqueness
  proof
    let H1,H2 be FinSequence of V;
    assume that
A5: len H1 = len F and
A6: for i st i in dom H1 holds H1.i = (F/.i) * f.(F/.i) and
A7: len H2 = len F and
A8: for i st i in dom H2 holds H2.i = (F/.i) * f.(F/.i);
    now
      let k be Nat;
      assume 1 <= k & k <= len H1;
      then
A9:   k in Seg(len H1) by FINSEQ_1:1;
      then k in dom H1 by FINSEQ_1:def 3;
      then
A10:  H1.k = (F/.k) * f.(F/.k) by A6;
      k in dom H2 by A5,A7,A9,FINSEQ_1:def 3;
      hence H1.k = H2.k by A8,A10;
    end;
    hence thesis by A5,A7,FINSEQ_1:14;
  end;
end;

theorem Th23:
  i in dom F & v = F.i implies (f (#) F).i = v * f.v
proof
  assume that
A1: i in dom F and
A2: v = F.i;
A3: F/.i = F.i by A1,PARTFUN1:def 6;
  len(f (#) F) = len F by Def6;
  then i in dom(f (#) F) by A1,FINSEQ_3:29;
  hence thesis by A2,A3,Def6;
end;

theorem
  f (#) <*>(the carrier of V) = <*>(the carrier of V)
proof
  len(f (#) <*>(the carrier of V)) = len(<*>(the carrier of V)) by Def6
    .= 0;
  hence thesis;
end;

theorem Th25:
  f (#) <* v *> = <* v * f.v *>
proof
A1: 1 in {1} by TARSKI:def 1;
A2: len(f (#) <* v *>) = len<* v *> by Def6
    .= 1 by FINSEQ_1:40;
  then dom(f (#) <* v *>) = {1} by FINSEQ_1:2,def 3;
  then (f (#) <* v *>).1 = (<* v *>/.1) * f.(<* v *>/.1) by A1,Def6
    .= v * f.(<* v *>/.1) by FINSEQ_4:16
    .= v * f.v by FINSEQ_4:16;
  hence thesis by A2,FINSEQ_1:40;
end;

theorem Th26:
  f (#) <* v1,v2 *> = <* v1 * f.v1, v2 * f.v2 *>
proof
A1: len(f (#) <* v1,v2 *>) = len<* v1,v2 *> by Def6
    .= 2 by FINSEQ_1:44;
  then
A2: dom(f (#) <* v1,v2 *>) = {1,2} by FINSEQ_1:2,def 3;
  2 in {1,2} by TARSKI:def 2;
  then
A3: (f (#) <* v1,v2 *>).2 = (<* v1,v2 *>/.2) * f.(<* v1,v2 *>/.2) by A2,Def6
    .= v2 * f.(<* v1,v2 *>/.2) by FINSEQ_4:17
    .= v2 * f.v2 by FINSEQ_4:17;
  1 in {1,2} by TARSKI:def 2;
  then (f (#) <* v1,v2 *>).1 = (<* v1,v2 *>/.1) * f.(<* v1,v2 *>/.1) by A2,Def6
    .= v1 * f.(<* v1,v2 *>/.1) by FINSEQ_4:17
    .= v1 * f.v1 by FINSEQ_4:17;
  hence thesis by A1,A3,FINSEQ_1:44;
end;

theorem
  f (#) <* v1,v2,v3 *> = <* v1 * f.v1, v2 * f.v2, v3 * f.v3 *>
proof
A1: len(f (#) <* v1,v2,v3 *>) = len<* v1,v2,v3 *> by Def6
    .= 3 by FINSEQ_1:45;
  then
A2: dom(f (#) <* v1,v2,v3 *>) = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
  3 in {1,2,3} by ENUMSET1:def 1;
  then
A3: (f (#) <* v1,v2,v3 *>).3 = (<* v1,v2,v3 *>/.3) * f.(<* v1,v2,v3 *>/.3)
  by A2,Def6
    .= v3 * f.(<* v1,v2,v3 *>/.3) by FINSEQ_4:18
    .= v3 * f.v3 by FINSEQ_4:18;
  2 in {1,2,3} by ENUMSET1:def 1;
  then
A4: (f (#) <* v1,v2,v3 *>).2 = (<* v1,v2,v3 *>/.2) * f.(<* v1,v2,v3 *>/.2)
  by A2,Def6
    .= v2 * f.(<* v1,v2,v3 *>/.2) by FINSEQ_4:18
    .= v2 * f.v2 by FINSEQ_4:18;
  1 in {1,2,3} by ENUMSET1:def 1;
  then (f (#) <* v1,v2,v3 *>).1 = (<* v1,v2,v3 *>/.1) * f.(<* v1,v2,v3 *>/.1)
  by A2,Def6
    .= v1 * f.(<* v1,v2,v3 *>/.1) by FINSEQ_4:18
    .= v1 * f.v1 by FINSEQ_4:18;
  hence thesis by A1,A4,A3,FINSEQ_1:45;
end;

theorem Th28:
  f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
proof
  set H = (f (#) F) ^ (f (#) G);
  set I = F ^ G;
A1: len F = len(f (#) F) by Def6;
A2: len H = len(f (#) F) + len(f (#) G) by FINSEQ_1:22
    .= len F + len(f (#) G) by Def6
    .= len F + len G by Def6
    .= len I by FINSEQ_1:22;
A3: len G = len(f (#) G) by Def6;
  now
    let k be Nat;
    assume
A4: k in dom H;
    now
      per cases by A4,FINSEQ_1:25;
      suppose
A5:     k in dom(f (#) F);
        then
A6:     k in dom F by A1,FINSEQ_3:29;
        then
A7:     k in dom(F ^ G) by FINSEQ_3:22;
A8:     F/.k = F.k by A6,PARTFUN1:def 6
          .= (F ^ G).k by A6,FINSEQ_1:def 7
          .= (F ^ G)/.k by A7,PARTFUN1:def 6;
        thus H.k = (f (#) F).k by A5,FINSEQ_1:def 7
          .= (I/.k) * f.(I/.k) by A5,A8,Def6;
      end;
      suppose
A9:     ex n be Nat st n in dom(f (#) G) & k = len(f (#) F) + n;
A10:    k in dom I by A2,A4,FINSEQ_3:29;
        consider n be Nat such that
A11:    n in dom(f (#) G) and
A12:    k = len(f (#) F) + n by A9;
A13:    n in dom G by A3,A11,FINSEQ_3:29;
        then
A14:    G/.n = G.n by PARTFUN1:def 6
          .= (F ^ G).k by A1,A12,A13,FINSEQ_1:def 7
          .= (F ^ G)/.k by A10,PARTFUN1:def 6;
        thus H.k = (f (#) G).n by A11,A12,FINSEQ_1:def 7
          .= (I/.k) * f.(I/.k) by A11,A14,Def6;
      end;
    end;
    hence H.k = (I/.k) * f.(I/.k);
  end;
  hence thesis by A2,Def6;
end;

definition
  let R, V, L;
  func Sum(L) -> Vector of V means
  :Def7:
  ex F st F is one-to-one & rng F = Carrier(L) & it = Sum(L (#) F);
  existence
  proof
    consider F being FinSequence such that
A1: rng F = Carrier(L) and
A2: F is one-to-one by FINSEQ_4:58;
    reconsider F as FinSequence of V by A1,FINSEQ_1:def 4;
    take Sum(L (#) F);
    take F;
    thus F is one-to-one & rng F = Carrier(L) by A1,A2;
    thus thesis;
  end;
  uniqueness
  proof
    let v1,v2;
    given F1 being FinSequence of V such that
A3: F1 is one-to-one and
A4: rng F1 = Carrier(L) and
A5: v1 = Sum(L (#) F1);
    given F2 being FinSequence of V such that
A6: F2 is one-to-one and
A7: rng F2 = Carrier(L) and
A8: v2 = Sum(L (#) F2);
    defpred P[set,set] means {$2} = F1 " {F2.$1};
A9: len F1 = len F2 by A3,A4,A6,A7,FINSEQ_1:48;
A10: dom F1 = Seg(len F1) by FINSEQ_1:def 3;
A11: dom F2 = Seg(len F2) by FINSEQ_1:def 3;
A12: for x st x in dom F1 ex y st y in dom F1 & P[x,y]
    proof
      let x;
      assume x in dom F1;
      then F2.x in rng F1 by A4,A7,A9,A10,A11,FUNCT_1:def 3;
      then consider y such that
A13:  F1 " {F2.x} = {y} by A3,FUNCT_1:74;
      take y;
      y in F1 " {F2.x} by A13,TARSKI:def 1;
      hence y in dom F1 by FUNCT_1:def 7;
      thus thesis by A13;
    end;
    consider f being Function of dom F1, dom F1 such that
A14: for x st x in dom F1 holds P[x,f.x] from FUNCT_2:sch 1(A12);
A15: rng f = dom F1
    proof
      thus rng f c= dom F1 by RELAT_1:def 19;
      let y;
      assume
A16:  y in dom F1;
      then F1.y in rng F2 by A4,A7,FUNCT_1:def 3;
      then consider x such that
A17:  x in dom F2 and
A18:  F2.x = F1.y by FUNCT_1:def 3;
      F1 " {F2.x} = F1 " Im(F1,y) by A16,A18,FUNCT_1:59;
      then F1 " {F2.x} c= {y} by A3,FUNCT_1:82;
      then {f.x} c= {y} by A9,A10,A11,A14,A17;
      then
A19:  f.x = y by ZFMISC_1:18;
      x in dom f by A9,A10,A11,A17,FUNCT_2:def 1;
      hence thesis by A19,FUNCT_1:def 3;
    end;
    set G1 = L (#) F1;
A20: len G1 = len F1 by Def6;
A21: dom F1 = {} implies dom F1 = {};
A22: f is one-to-one
    proof
      let y1,y2 be set;
      assume that
A23:  y1 in dom f and
A24:  y2 in dom f and
A25:  f.y1 = f.y2;
A26:  y2 in dom F1 by A21,A24,FUNCT_2:def 1;
      then
A27:  F1 " {F2.y2} = {f.y2} by A14;
A28:  y1 in dom F1 by A21,A23,FUNCT_2:def 1;
      then F2.y1 in rng F1 by A4,A7,A9,A10,A11,FUNCT_1:def 3;
      then
A29:  {F2.y1} c= rng F1 by ZFMISC_1:31;
      F2.y2 in rng F1 by A4,A7,A9,A10,A11,A26,FUNCT_1:def 3;
      then
A30:  {F2.y2} c= rng F1 by ZFMISC_1:31;
      F1 " {F2.y1} = {f.y1} by A14,A28;
      then {F2.y1} = {F2.y2} by A25,A27,A29,A30,FUNCT_1:91;
      then
A31:  F2.y1 = F2.y2 by ZFMISC_1:3;
      y1 in dom F2 & y2 in dom F2 by A9,A10,A11,A21,A23,A24,FUNCT_2:def 1;
      hence thesis by A6,A31,FUNCT_1:def 4;
    end;
    set G2 = L (#) F2;
A32: dom G2 = Seg(len G2) by FINSEQ_1:def 3;
    reconsider f as Permutation of dom F1 by A15,A22,FUNCT_2:57;
    dom F1 = Seg len F1 & dom G1 = Seg len G1 by FINSEQ_1:def 3;
    then reconsider f as Permutation of dom G1 by A20;
A33: len G2 = len F2 by Def6;
A34: dom(G1) = Seg(len G1) by FINSEQ_1:def 3;
    now
      let i be Element of NAT;
      assume
A35:  i in dom G2;
      then
A36:  G2.i = (F2/.i) * L.(F2/.i) & F2.i = F2/.i by A33,A11,A32,Def6,
PARTFUN1:def 6;
      i in dom F2 by A33,A35,FINSEQ_3:29;
      then reconsider u = F2.i as Vector of V by FINSEQ_2:11;
      i in dom f by A9,A20,A33,A34,A32,A35,FUNCT_2:def 1;
      then
A37:  f.i in dom F1 by A15,FUNCT_1:def 3;
      then reconsider m = f.i as Element of NAT by A10;
      reconsider v = F1.m as Vector of V by A37,FINSEQ_2:11;
      {F1.(f.i)} = Im(F1,f.i) by A37,FUNCT_1:59
        .= F1 .: (F1 " {F2.i}) by A9,A33,A10,A32,A14,A35;
      then
A38:  u = v by FUNCT_1:75,ZFMISC_1:18;
      F1.m = F1/.m by A37,PARTFUN1:def 6;
      hence G2.i = G1.(f.i) by A20,A10,A34,A37,A38,A36,Def6;
    end;
    hence thesis by A3,A4,A5,A6,A7,A8,A20,A33,FINSEQ_1:48,RLVECT_2:6;
  end;
end;

Lm3: Sum(ZeroLC(V)) = 0.V
proof
  consider F such that
  F is one-to-one and
A1: rng F = Carrier(ZeroLC(V)) and
A2: Sum(ZeroLC(V)) = Sum(ZeroLC(V) (#) F) by Def7;
  Carrier(ZeroLC(V)) = {} by Def4;
  then F = {} by A1,RELAT_1:41;
  then len F = 0;
  then len(ZeroLC(V) (#) F) = 0 by Def6;
  hence thesis by A2,RLVECT_1:75;
end;

theorem Th29:
  0.R <> 1_R implies (A <> {} & A is linearly-closed iff for l
  holds Sum l in A)
proof
  assume
A1: 0.R <> 1_R;
  thus A <> {} & A is linearly-closed implies for l holds Sum(l) in A
  proof
    defpred P[Nat] means for l st card(Carrier(l)) = $1 holds Sum (l) in A;
    assume that
A2: A <> {} and
A3: A is linearly-closed;
    now
      let l;
      assume card(Carrier(l)) = 0;
      then Carrier(l) = {};
      then l = ZeroLC(V) by Def4;
      then Sum(l) = 0.V by Lm3;
      hence Sum(l) in A by A2,A3,RMOD_2:1;
    end;
    then
A4: P[0];
    now
      let k be Element of NAT;
      assume
A5:   for l st card Carrier l = k holds Sum(l) in A;
      let l;
      deffunc Q(Element of V) = l.$1;
      consider F such that
A6:   F is one-to-one and
A7:   rng F = Carrier(l) and
A8:   Sum(l) = Sum(l (#) F) by Def7;
      reconsider G = F | Seg k as FinSequence of V by FINSEQ_1:18;
      assume
A9:   card Carrier l = k + 1;
      then
A10:  len F = k + 1 by A6,A7,FINSEQ_4:62;
      then
A11:  len(l (#) F) = k + 1 by Def6;
A12:  k + 1 in Seg(k + 1) by FINSEQ_1:4;
      then
A13:  k + 1 in dom F by A10,FINSEQ_1:def 3;
      k + 1 in dom F by A10,A12,FINSEQ_1:def 3;
      then reconsider v = F.(k + 1) as Vector of V by FINSEQ_2:11;
      consider f being Function of V, R such that
A14:  f.v = 0.R and
A15:  for u being Element of V st u <> v holds f.u = Q(u) from
      FUNCT_2:sch 6;
      reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
A16:  v in Carrier(l) by A7,A13,FUNCT_1:def 3;
      now
        let u;
        assume
A17:    not u in Carrier(l);
        hence f.u = l.u by A16,A15
          .= 0.R by A17;
      end;
      then reconsider f as Linear_Combination of V by Def2;
A18:  A \ {v} c= A by XBOOLE_1:36;
A19:  Carrier(l) c= A by Def5;
      then
A20:  v * l.v in A by A3,A16,RMOD_2:def 1;
A21:  Carrier(f) = Carrier(l) \ {v}
      proof
        thus Carrier(f) c= Carrier(l) \ {v}
        proof
          let x;
          assume x in Carrier(f);
          then consider u such that
A22:      u = x and
A23:      f.u <> 0.R;
          f.u = l.u by A14,A15,A23;
          then
A24:      x in Carrier(l) by A22,A23;
          not x in {v} by A14,A22,A23,TARSKI:def 1;
          hence thesis by A24,XBOOLE_0:def 5;
        end;
        let x;
        assume
A25:    x in Carrier(l) \ {v};
        then x in Carrier(l) by XBOOLE_0:def 5;
        then consider u such that
A26:    x = u and
A27:    l.u <> 0.R;
        not x in {v} by A25,XBOOLE_0:def 5;
        then x <> v by TARSKI:def 1;
        then l.u = f.u by A15,A26;
        hence thesis by A26,A27;
      end;
      then Carrier(f) c= A \ {v} by A19,XBOOLE_1:33;
      then Carrier(f) c= A by A18,XBOOLE_1:1;
      then reconsider f as Linear_Combination of A by Def5;
A28:  len G = k by A10,FINSEQ_3:53;
      then
A29:  len (f (#) G) = k by Def6;
A30:  rng G = Carrier(f)
      proof
        thus rng G c= Carrier f
        proof
          let x;
          assume x in rng G;
          then consider y such that
A31:      y in dom G and
A32:      G.y = x by FUNCT_1:def 3;
          reconsider y as Nat by A31,FINSEQ_3:23;
A33:      dom G c= dom F & G.y = F.y by A31,FUNCT_1:47,RELAT_1:60;
          now
            assume x = v;
            then
A34:        k + 1 = y by A6,A13,A31,A32,A33,FUNCT_1:def 4;
            y <= k by A28,A31,FINSEQ_3:25;
            hence contradiction by A34,XREAL_1:29;
          end;
          then
A35:      not x in {v} by TARSKI:def 1;
          x in rng F by A31,A32,A33,FUNCT_1:def 3;
          hence thesis by A7,A21,A35,XBOOLE_0:def 5;
        end;
        let x;
        assume
A36:    x in Carrier(f);
        then x in rng F by A7,A21,XBOOLE_0:def 5;
        then consider y such that
A37:    y in dom F and
A38:    F.y = x by FUNCT_1:def 3;
        reconsider y as Element of NAT by A37,FINSEQ_3:23;
        now
          assume not y in Seg k;
          then y in dom F \ Seg k by A37,XBOOLE_0:def 5;
          then y in Seg(k + 1) \ Seg k by A10,FINSEQ_1:def 3;
          then y in {k + 1} by FINSEQ_3:15;
          then y = k + 1 by TARSKI:def 1;
          then not v in {v} by A21,A36,A38,XBOOLE_0:def 5;
          hence contradiction by TARSKI:def 1;
        end;
        then y in dom F /\ Seg k by A37,XBOOLE_0:def 4;
        then
A39:    y in dom G by RELAT_1:61;
        then G.y = F.y by FUNCT_1:47;
        hence thesis by A38,A39,FUNCT_1:def 3;
      end;
      Seg(k + 1) /\ Seg k = Seg k by FINSEQ_1:7,NAT_1:12
        .= dom(f (#) G) by A29,FINSEQ_1:def 3;
      then
A40:  dom(f (#) G) = dom(l (#) F) /\ Seg k by A11,FINSEQ_1:def 3;
      now
        let x;
A41:    rng F c= the carrier of V by FINSEQ_1:def 4;
        assume
A42:    x in dom(f (#) G);
        then reconsider n = x as Nat by FINSEQ_3:23;
        n in dom(l (#) F) by A40,A42,XBOOLE_0:def 4;
        then
A43:    n in dom F by A10,A11,FINSEQ_3:29;
        then F.n in rng F by FUNCT_1:def 3;
        then reconsider w = F.n as Vector of V by A41;
A44:    n in dom G by A28,A29,A42,FINSEQ_3:29;
        then
A45:    G.n in rng G by FUNCT_1:def 3;
        rng G c= the carrier of V by FINSEQ_1:def 4;
        then reconsider u = G.n as Vector of V by A45;
        not u in {v} by A21,A30,A45,XBOOLE_0:def 5;
        then
A46:    u <> v by TARSKI:def 1;
A47:    (f (#) G).n = u * f.u by A44,Th23
          .= u * l.u by A15,A46;
        w = u by A44,FUNCT_1:47;
        hence (f (#) G).x = (l (#) F).x by A47,A43,Th23;
      end;
      then f (#) G = (l (#) F) | Seg k by A40,FUNCT_1:46;
      then
A48:  f (#) G = (l (#) F) | dom (f (#) G) by A29,FINSEQ_1:def 3;
      v in rng F by A13,FUNCT_1:def 3;
      then {v} c= Carrier(l) by A7,ZFMISC_1:31;
      then card(Carrier(f)) = k + 1 - card{v} by A9,A21,CARD_2:44
        .= k + 1 - 1 by CARD_1:30
        .= k by XCMPLX_1:26;
      then
A49:  Sum(f) in A by A5;
      G is one-to-one by A6,FUNCT_1:52;
      then
A50:  Sum(f (#) G) = Sum(f) by A30,Def7;
      (l (#) F).(len F) = v * l.v by A10,A13,Th23;
      then Sum(l (#) F) = Sum (f (#) G) + v * l.v by A10,A11,A29,A48,
RLVECT_1:38;
      hence Sum(l) in A by A3,A8,A20,A50,A49,RMOD_2:def 1;
    end;
    then
A51: for k be Element of NAT st P[k] holds P[k+1];
    let l;
A52: card Carrier l = card Carrier l;
    for k be Element of NAT holds P[k] from NAT_1:sch 1(A4,A51);
    hence thesis by A52;
  end;
  assume
A53: for l holds Sum(l) in A;
  hence A <> {};
  ZeroLC(V) is Linear_Combination of A & Sum(ZeroLC(V)) = 0.V by Lm3,Th20;
  then
A54: 0.V in A by A53;
A55: for a,v st v in A holds v * a in A
  proof
    let a,v;
    assume
A56: v in A;
    now
      per cases;
      suppose
        a = 0.R;
        hence thesis by A54,VECTSP_2:32;
      end;
      suppose
A57:    a <> 0.R;
        deffunc F(Element of V)=0.R;
        consider f such that
A58:    f.v = a and
A59:    for u being Element of V st u <> v holds f.u = F(u) from
        FUNCT_2:sch 6;
        reconsider f as Element of Funcs(the carrier of V, the carrier of R)
        by FUNCT_2:8;
        now
          let u;
          assume not u in {v};
          then u <> v by TARSKI:def 1;
          hence f.u = 0.R by A59;
        end;
        then reconsider f as Linear_Combination of V by Def2;
A60:    Carrier(f) = {v}
        proof
          thus Carrier(f) c= {v}
          proof
            let x;
            assume x in Carrier(f);
            then consider u such that
A61:        x = u and
A62:        f.u <> 0.R;
            u = v by A59,A62;
            hence thesis by A61,TARSKI:def 1;
          end;
          let x;
          assume x in {v};
          then x = v by TARSKI:def 1;
          hence thesis by A57,A58;
        end;
        {v} c= A by A56,ZFMISC_1:31;
        then reconsider f as Linear_Combination of A by A60,Def5;
        consider F such that
A63:    F is one-to-one & rng F = Carrier(f) and
A64:    Sum(f (#) F) = Sum(f) by Def7;
        F = <* v *> by A60,A63,FINSEQ_3:97;
        then f (#) F = <* v * f.v *> by Th25;
        then Sum(f) = v * a by A58,A64,RLVECT_1:44;
        hence thesis by A53;
      end;
    end;
    hence thesis;
  end;
  thus for v,u st v in A & u in A holds v + u in A
  proof
    let v,u;
    assume that
A65: v in A and
A66: u in A;
    now
      per cases;
      suppose
        u = v;
        then v + u = v * 1_R + v by VECTSP_2:def 9
          .= v * 1_R + v * 1_R by VECTSP_2:def 9
          .= v * (1_R + 1_R) by VECTSP_2:def 9;
        hence thesis by A55,A65;
      end;
      suppose
A67:    v <> u;
        deffunc F(Element of V)=0.R;
        consider f such that
A68:    f.v = 1_R & f.u = 1_R and
A69:    for w being Element of V st w <> v & w <> u holds f.w = F(w)
        from FUNCT_2:sch 7(A67);
        reconsider f as Element of Funcs(the carrier of V, the carrier of R)
        by FUNCT_2:8;
        now
          let w;
          assume not w in {v,u};
          then w <> v & w <> u by TARSKI:def 2;
          hence f.w = 0.R by A69;
        end;
        then reconsider f as Linear_Combination of V by Def2;
A70:    Carrier(f) = {v,u}
        proof
          thus Carrier(f) c= {v,u}
          proof
            let x;
            assume x in Carrier(f);
            then ex w st x = w & f.w <> 0.R;
            then x = v or x = u by A69;
            hence thesis by TARSKI:def 2;
          end;
          let x;
          assume x in {v,u};
          then x = v or x = u by TARSKI:def 2;
          hence thesis by A1,A68;
        end;
        then
A71:    Carrier(f) c= A by A65,A66,ZFMISC_1:32;
A72:    u * 1_R = u & v * 1_R = v by VECTSP_2:def 9;
        reconsider f as Linear_Combination of A by A71,Def5;
        consider F such that
A73:    F is one-to-one & rng F = Carrier(f) and
A74:    Sum(f (#) F) = Sum(f) by Def7;
        F = <* v,u *> or F = <* u,v *> by A67,A70,A73,FINSEQ_3:99;
        then f (#) F = <* v * 1_R, u * 1_R *> or f (#) F = <* u * 1_R, v *
        1_R *> by A68,Th26;
        then Sum(f) = v + u by A74,A72,RLVECT_1:45;
        hence thesis by A53;
      end;
    end;
    hence thesis;
  end;
  thus thesis by A55;
end;

theorem
  Sum(ZeroLC(V)) = 0.V by Lm3;

theorem Th31:
  for l being Linear_Combination of {}(the carrier of V) holds Sum (l) = 0.V
proof
  let l be Linear_Combination of {}(the carrier of V);
  l = ZeroLC(V) by Th21;
  hence thesis by Lm3;
end;

theorem Th32:
  for l being Linear_Combination of {v} holds Sum(l) = v * l.v
proof
  let l be Linear_Combination of {v};
A1: Carrier(l) c= {v} by Def5;
  now
    per cases by A1,ZFMISC_1:33;
    suppose
      Carrier(l) = {};
      then
A2:   l = ZeroLC(V) by Def4;
      hence Sum(l) = 0.V by Lm3
        .= v * 0.R by VECTSP_2:32
        .= v * l.v by A2,Th18;
    end;
    suppose
      Carrier(l) = {v};
      then consider F such that
A3:   F is one-to-one & rng F = {v} and
A4:   Sum(l) = Sum(l (#) F) by Def7;
      F = <* v *> by A3,FINSEQ_3:97;
      then l (#) F = <* v * l.v *> by Th25;
      hence thesis by A4,RLVECT_1:44;
    end;
  end;
  hence thesis;
end;

theorem Th33:
  v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds
  Sum (l) = v1 * l.v1 + v2 * l.v2
proof
  assume
A1: v1 <> v2;
  let l be Linear_Combination of {v1,v2};
A2: Carrier(l) c= {v1,v2} by Def5;
  now
    per cases by A2,ZFMISC_1:36;
    suppose
      Carrier(l) = {};
      then
A3:   l = ZeroLC(V) by Def4;
      hence Sum(l) = 0.V by Lm3
        .= 0.V + 0.V by RLVECT_1:def 4
        .= v1 * 0.R + 0.V by VECTSP_2:32
        .= v1 * 0.R + v2 * 0.R by VECTSP_2:32
        .= v1 * l.v1 + v2 * 0.R by A3,Th18
        .= v1 * l.v1 + v2 * l.v2 by A3,Th18;
    end;
    suppose
A4:   Carrier(l) = {v1};
      then reconsider L = l as Linear_Combination of {v1} by Def5;
A5:   not v2 in Carrier(l) by A1,A4,TARSKI:def 1;
      thus Sum(l) = Sum(L) .= v1 * l.v1 by Th32
        .= v1 * l.v1 + 0.V by RLVECT_1:def 4
        .= v1 * l.v1 + v2 * 0.R by VECTSP_2:32
        .= v1 * l.v1 + v2 * l.v2 by A5;
    end;
    suppose
A6:   Carrier(l) = {v2};
      then reconsider L = l as Linear_Combination of {v2} by Def5;
A7:   not v1 in Carrier(l) by A1,A6,TARSKI:def 1;
      thus Sum(l) = Sum(L) .= v2 * l.v2 by Th32
        .= 0.V + v2 * l.v2 by RLVECT_1:def 4
        .= v1 * 0.R + v2 * l.v2 by VECTSP_2:32
        .= v1 * l.v1 + v2 * l.v2 by A7;
    end;
    suppose
      Carrier(l) = {v1,v2};
      then consider F such that
A8:   F is one-to-one & rng F = {v1,v2} and
A9:   Sum(l) = Sum(l (#) F) by Def7;
      F = <* v1,v2 *> or F = <* v2,v1 *> by A1,A8,FINSEQ_3:99;
      then l (#) F = <* v1 * l.v1, v2 * l.v2 *> or l (#) F = <* v2 * l.v2, v1
      * l.v1 *> by Th26;
      hence thesis by A9,RLVECT_1:45;
    end;
  end;
  hence thesis;
end;

theorem
  Carrier(L) = {} implies Sum(L) = 0.V
proof
  assume Carrier(L) = {};
  then L = ZeroLC(V) by Def4;
  hence thesis by Lm3;
end;

theorem Th35:
  Carrier(L) = {v} implies Sum(L) = v * L.v
proof
  assume Carrier(L) = {v};
  then L is Linear_Combination of {v} by Def5;
  hence thesis by Th32;
end;

theorem
  Carrier(L) = {v1,v2} & v1 <> v2 implies Sum(L) = v1 * L.v1 + v2 * L.v2
proof
  assume that
A1: Carrier(L) = {v1,v2} and
A2: v1 <> v2;
  L is Linear_Combination of {v1,v2} by A1,Def5;
  hence thesis by A2,Th33;
end;

definition
  let R, V, L1, L2;
  redefine pred L1 = L2 means
  for v holds L1.v = L2.v;
  compatibility by FUNCT_2:63;
end;

definition
  let R, V, L1, L2;
  func L1 + L2 -> Linear_Combination of V means
  :Def9:
  for v holds it.v = L1. v + L2.v;
  existence
  proof
    deffunc F(Element of V)=L1.$1 + L2.$1;
    consider f being Function of V, R such that
A1: for v being Element of V holds f.v = F(v) from FUNCT_2:sch 4;
    reconsider f as Element of Funcs(the carrier of V,the carrier of R) by
FUNCT_2:8;
    now
      let v;
      assume
A2:   not v in (Carrier(L1) \/ Carrier(L2));
      then not v in Carrier(L2) by XBOOLE_0:def 3;
      then
A3:   L2.v = 0.R;
      not v in Carrier(L1) by A2,XBOOLE_0:def 3;
      then L1.v = 0.R;
      hence f.v = 0.R + 0.R by A1,A3
        .= 0.R by RLVECT_1:4;
    end;
    then reconsider f as Linear_Combination of V by Def2;
    take f;
    let v;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let M,N be Linear_Combination of V;
    assume
A4: for v holds M.v = L1.v + L2.v;
    assume
A5: for v holds N.v = L1.v + L2.v;
    let v;
    thus M.v = L1.v + L2.v by A4
      .= N.v by A5;
  end;
end;

theorem Th37:
  Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2)
proof
  let x;
  assume x in Carrier(L1 + L2);
  then consider u such that
A1: x = u and
A2: (L1 + L2).u <> 0.R;
  (L1 + L2).u = L1.u + L2.u by Def9;
  then L1.u <> 0.R or L2.u <> 0.R by A2,RLVECT_1:4;
  then x in {v1 : L1.v1 <> 0.R} or x in {v2 : L2.v2 <> 0.R} by A1;
  hence thesis by XBOOLE_0:def 3;
end;

theorem Th38:
  L1 is Linear_Combination of A & L2 is Linear_Combination of A
  implies L1 + L2 is Linear_Combination of A
proof
  assume L1 is Linear_Combination of A & L2 is Linear_Combination of A;
  then Carrier(L1) c= A & Carrier(L2) c= A by Def5;
  then
A1: Carrier(L1) \/ Carrier(L2) c= A by XBOOLE_1:8;
  Carrier(L1 + L2) c= Carrier(L1) \/ Carrier(L2) by Th37;
  hence Carrier(L1 + L2) c= A by A1,XBOOLE_1:1;
end;

theorem Th39:
  for R being comRing for V being RightMod of R for L1, L2 being
  Linear_Combination of V holds L1 + L2 = L2 + L1
proof
  let R be comRing;
  let V be RightMod of R;
  let L1, L2 be Linear_Combination of V;
  let v be Vector of V;
  thus (L1 + L2).v = L2.v + L1.v by Def9
    .= (L2 + L1).v by Def9;
end;

theorem
  L1 + (L2 + L3) = L1 + L2 + L3
proof
  let v;
  thus (L1 + (L2 + L3)).v = L1.v + (L2 + L3).v by Def9
    .= L1.v + (L2.v + L3.v) by Def9
    .= L1.v + L2.v + L3.v by RLVECT_1:def 3
    .= (L1 + L2).v + L3.v by Def9
    .= (L1 + L2 + L3).v by Def9;
end;

theorem
  for R being comRing for V being RightMod of R for L being
  Linear_Combination of V holds L + ZeroLC(V) = L & ZeroLC(V) + L = L
proof
  let R be comRing;
  let V be RightMod of R;
  let L be Linear_Combination of V;
  thus L + ZeroLC(V) = L
  proof
    let v be Vector of V;
    thus (L + ZeroLC(V)).v = L.v + ZeroLC(V).v by Def9
      .= L.v + 0.R by Th18
      .= L.v by RLVECT_1:4;
  end;
  hence thesis by Th39;
end;

definition
  let R, V, a, L;
  func L * a -> Linear_Combination of V means
  :Def10:
  for v holds it.v = L.v * a;
  existence
  proof
    deffunc F(Element of V)=L.$1 * a;
    consider f being Function of V, R such that
A1: for v being Element of V holds f.v = F(v) from FUNCT_2:sch 4;
    reconsider f as Element of Funcs(the carrier of V,the carrier of R) by
FUNCT_2:8;
    now
      let v;
      assume not v in Carrier(L);
      then L.v = 0.R;
      hence f.v = 0.R * a by A1
        .= 0.R by VECTSP_1:7;
    end;
    then reconsider f as Linear_Combination of V by Def2;
    take f;
    let v;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let L1,L2;
    assume
A2: for v holds L1.v = L.v * a;
    assume
A3: for v holds L2.v = L.v * a;
    let v;
    thus L1.v = L.v * a by A2
      .= L2.v by A3;
  end;
end;

theorem Th42:
  Carrier(L * a) c= Carrier(L)
proof
  set T = {u : (L * a).u <> 0.R};
  set S = {v : L.v <> 0.R};
  T c= S
  proof
    let x;
    assume x in T;
    then consider u such that
A1: x = u and
A2: (L * a).u <> 0.R;
    (L * a).u = L.u * a by Def10;
    then L.u <> 0.R by A2,VECTSP_1:7;
    hence thesis by A1;
  end;
  hence thesis;
end;

reserve RR for domRing;
reserve VV for RightMod of RR;
reserve LL for Linear_Combination of VV;
reserve aa for Scalar of RR;
reserve uu, vv for Vector of VV;

theorem Th43:
  aa <> 0.RR implies Carrier(LL * aa) = Carrier(LL)
proof
  set T = {uu : (LL * aa).uu <> 0.RR};
  set S = {vv : LL.vv <> 0.RR};
  assume
A1: aa <> 0.RR;
  T = S
  proof
    thus T c= S
    proof
      let x;
      assume x in T;
      then consider uu such that
A2:   x = uu and
A3:   (LL * aa).uu <> 0.RR;
      (LL * aa).uu = LL.uu * aa by Def10;
      then LL.uu <> 0.RR by A3,VECTSP_1:6;
      hence thesis by A2;
    end;
    let x;
    assume x in S;
    then consider vv such that
A4: x = vv and
A5: LL.vv <> 0.RR;
    (LL * aa).vv = LL.vv * aa by Def10;
    then (LL * aa).vv <> 0.RR by A1,A5,VECTSP_2:def 1;
    hence thesis by A4;
  end;
  hence thesis;
end;

theorem Th44:
  L * 0.R = ZeroLC(V)
proof
  let v;
  thus (L * 0.R).v = L.v * 0.R by Def10
    .= 0.R by VECTSP_1:6
    .= ZeroLC(V).v by Th18;
end;

theorem Th45:
  L is Linear_Combination of A implies L * a is Linear_Combination of A
proof
  assume L is Linear_Combination of A;
  then
A1: Carrier(L) c= A by Def5;
  Carrier(L * a) c= Carrier(L) by Th42;
  then Carrier(L * a) c= A by A1,XBOOLE_1:1;
  hence thesis by Def5;
end;

theorem
  L * (a + b) = L * a + L * b
proof
  let v;
  thus (L * (a + b)).v = L.v * (a + b) by Def10
    .= L.v * a + L.v * b by VECTSP_1:def 7
    .= (L * a).v + L.v * b by Def10
    .= (L * a).v + (L * b).v by Def10
    .= ((L * a) + (L * b)).v by Def9;
end;

theorem
  (L1 + L2) * a = L1 * a + L2 * a
proof
  let v;
  thus ((L1 + L2) * a).v = (L1 + L2).v * a by Def10
    .= (L1.v + L2.v) * a by Def9
    .= L1.v * a + L2.v * a by VECTSP_1:def 7
    .= (L1 * a).v + L2.v * a by Def10
    .= (L1 * a).v + (L2 * a). v by Def10
    .= ((L1 * a) + (L2 * a)).v by Def9;
end;

theorem Th48:
  (L * b) * a = L * (b * a)
proof
  let v;
  thus ((L * b) * a).v = (L * b).v * a by Def10
    .= L.v * b * a by Def10
    .= L.v * (b * a) by GROUP_1:def 3
    .= (L * (b * a)).v by Def10;
end;

theorem
  L * 1_R = L
proof
  let v;
  thus (L * 1_R).v = L.v * 1_R by Def10
    .= L.v by VECTSP_1:def 4;
end;

definition
  let R, V, L;
  func - L -> Linear_Combination of V equals
  L * (- 1_R);
  correctness;
  involutiveness
  proof
    let L, L9 be Linear_Combination of V;
    assume
A1: L = L9 * (- 1_R);
    let v;
    thus L9.v = L9.v * (1_R) by VECTSP_1:def 4
      .= L9.v * ((1_R) * (1_R)) by VECTSP_1:def 4
      .= L9.v * ((- 1_R) * (- 1_R)) by VECTSP_1:10
      .= (L9 * ((- 1_R) * (- 1_R))).v by Def10
      .= (L * (- 1_R)).v by A1,Th48;
  end;
end;

theorem Th50:
  (- L).v = - L.v
proof
  thus (- L).v = L.v * (- 1_R) by Def10
    .= - L.v by VECTSP_2:28;
end;

theorem
  L1 + L2 = ZeroLC(V) implies L2 = - L1
proof
  assume
A1: L1 + L2 = ZeroLC(V);
  let v;
  L1.v + L2.v = ZeroLC(V).v by A1,Def9
    .= 0.R by Th18;
  hence L2.v = - L1.v by RLVECT_1:6
    .= (- L1).v by Th50;
end;

theorem Th52:
  Carrier(- L) = Carrier(L)
proof
  set a = -1_R;
  Carrier(L * a) = Carrier(L)
  proof
    set S = {v : L.v <> 0.R};
    set T = {u : (L * a).u <> 0.R};
    T = S
    proof
      thus T c= S
      proof
        let x;
        assume x in T;
        then consider u such that
A1:     x = u and
A2:     (L * a).u <> 0.R;
        (L * a).u = L.u * a by Def10;
        then L.u <> 0.R by A2,VECTSP_1:7;
        hence thesis by A1;
      end;
      let x;
      assume x in S;
      then consider v such that
A3:   x = v and
A4:   L.v <> 0.R;
      (L * a).v = L.v * a by Def10
        .= -(L.v) by VECTSP_2:28;
      then (L * a).v <> 0.R by A4,VECTSP_2:3;
      hence thesis by A3;
    end;
    hence thesis;
  end;
  hence thesis;
end;

theorem
  L is Linear_Combination of A implies - L is Linear_Combination of A by Th45;

definition
  let R, V, L1, L2;
  func L1 - L2 -> Linear_Combination of V equals
  L1 + (- L2);
  correctness;
end;

theorem Th54:
  (L1 - L2).v = L1.v - L2.v
proof
  thus (L1 - L2).v = L1.v + (- L2).v by Def9
    .= L1.v + (- L2.v) by Th50
    .= L1.v - L2.v by RLVECT_1:def 11;
end;

theorem
  Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(L2)
proof
  Carrier(L1 - L2) c= Carrier(L1) \/ Carrier(- L2) by Th37;
  hence thesis by Th52;
end;

theorem
  L1 is Linear_Combination of A & L2 is Linear_Combination of A implies
  L1 - L2 is Linear_Combination of A
proof
  assume that
A1: L1 is Linear_Combination of A and
A2: L2 is Linear_Combination of A;
  - L2 is Linear_Combination of A by A2,Th45;
  hence thesis by A1,Th38;
end;

theorem
  L - L = ZeroLC(V)
proof
  let v;
  thus (L - L).v = L.v - L.v by Th54
    .= 0.R by RLVECT_1:15
    .= ZeroLC(V).v by Th18;
end;

theorem Th58:
  Sum(L1 + L2) = Sum(L1) + Sum(L2)
proof
  set A = Carrier(L1 + L2) \/ Carrier(L1) \/ Carrier(L2);
  set C1 = A \ Carrier(L1);
  consider p such that
A1: rng p = C1 and
A2: p is one-to-one by FINSEQ_4:58;
  reconsider p as FinSequence of V by A1,FINSEQ_1:def 4;
A3: A = Carrier(L1) \/ (Carrier(L1 + L2) \/ Carrier(L2)) by XBOOLE_1:4;
  set C3 = A \ Carrier(L1 + L2);
  consider r such that
A4: rng r = C3 and
A5: r is one-to-one by FINSEQ_4:58;
  reconsider r as FinSequence of V by A4,FINSEQ_1:def 4;
A6: A = Carrier(L1 + L2) \/ (Carrier(L1) \/ Carrier(L2)) by XBOOLE_1:4;
  set C2 = A \ Carrier(L2);
  consider q such that
A7: rng q = C2 and
A8: q is one-to-one by FINSEQ_4:58;
  reconsider q as FinSequence of V by A7,FINSEQ_1:def 4;
  consider F such that
A9: F is one-to-one and
A10: rng F = Carrier(L1 + L2) and
A11: Sum((L1 + L2) (#) F) = Sum(L1 + L2) by Def7;
  set FF = F ^ r;
  consider G such that
A12: G is one-to-one and
A13: rng G = Carrier(L1) and
A14: Sum(L1 (#) G) = Sum(L1) by Def7;
  rng FF = rng F \/ rng r by FINSEQ_1:31;
  then rng FF = Carrier(L1 + L2) \/ A by A10,A4,XBOOLE_1:39;
  then
A15: rng FF = A by A6,XBOOLE_1:7,12;
  set GG = G ^ p;
  rng GG = rng G \/ rng p by FINSEQ_1:31;
  then rng GG = Carrier(L1) \/ A by A13,A1,XBOOLE_1:39;
  then
A16: rng GG = A by A3,XBOOLE_1:7,12;
  rng F misses rng r
  proof
    set x = the Element of rng F /\ rng r;
    assume not thesis;
    then rng F /\ rng r <> {} by XBOOLE_0:def 7;
    then x in Carrier(L1 + L2) & x in C3 by A10,A4,XBOOLE_0:def 4;
    hence thesis by XBOOLE_0:def 5;
  end;
  then
A17: FF is one-to-one by A9,A5,FINSEQ_3:91;
  rng G misses rng p
  proof
    set x = the Element of rng G /\ rng p;
    assume not thesis;
    then rng G /\ rng p <> {} by XBOOLE_0:def 7;
    then x in Carrier(L1) & x in C1 by A13,A1,XBOOLE_0:def 4;
    hence thesis by XBOOLE_0:def 5;
  end;
  then
A18: GG is one-to-one by A12,A2,FINSEQ_3:91;
  then
A19: len GG = len FF by A17,A16,A15,FINSEQ_1:48;
  deffunc Q(Nat)=FF <- (GG.$1);
  consider P being FinSequence such that
A20: len P = len FF and
A21: for k be Nat st k in dom P holds P.k = Q(k) from FINSEQ_1:sch 2;
A22: dom P = Seg len FF by A20,FINSEQ_1:def 3;
A23: now
    let x;
    assume
A24: x in dom GG;
    then reconsider n = x as Nat by FINSEQ_3:23;
    GG.n in rng FF by A16,A15,A24,FUNCT_1:def 3;
    then
A25: FF just_once_values GG.n by A17,FINSEQ_4:8;
    n in Seg(len FF) by A19,A24,FINSEQ_1:def 3;
    then FF.(P.n) = FF.(FF <- (GG.n)) by A21,A22
      .= GG.n by A25,FINSEQ_4:def 3;
    hence GG.x = FF.(P.x);
  end;
A26: dom GG = dom FF by A19,FINSEQ_3:29;
A27: rng P c= dom FF
  proof
    let x;
    assume x in rng P;
    then consider y such that
A28: y in dom P and
A29: P.y = x by FUNCT_1:def 3;
    reconsider y as Nat by A28,FINSEQ_3:23;
    y in dom FF by A20,A28,FINSEQ_3:29;
    then GG.y in rng FF by A16,A15,A26,FUNCT_1:def 3;
    then
A30: FF just_once_values GG.y by A17,FINSEQ_4:8;
    P.y = FF <- (GG.y) by A21,A28;
    hence thesis by A29,A30,FINSEQ_4:def 3;
  end;
  now
    let x;
    thus x in dom GG implies x in dom P & P.x in dom FF
    proof
      assume x in dom GG;
      hence x in dom P by A19,A20,FINSEQ_3:29;
      then P.x in rng P by FUNCT_1:def 3;
      hence thesis by A27;
    end;
    assume that
A31: x in dom P and
    P.x in dom FF;
    x in Seg(len P) by A31,FINSEQ_1:def 3;
    hence x in dom GG by A19,A20,FINSEQ_1:def 3;
  end;
  then
A32: GG = FF * P by A23,FUNCT_1:10;
  dom FF c= rng P
  proof
    set f = FF" * GG;
    let x;
    assume
A33: x in dom FF;
    dom(FF") = rng GG by A17,A16,A15,FUNCT_1:33;
    then
A34: rng f = rng(FF") by RELAT_1:28
      .= dom FF by A17,FUNCT_1:33;
    f = FF " * FF * P by A32,RELAT_1:36
      .= id(dom FF) * P by A17,FUNCT_1:39
      .= P by A27,RELAT_1:53;
    hence thesis by A33,A34;
  end;
  then
A35: dom FF = rng P by A27,XBOOLE_0:def 10;
A36: len r = len((L1 + L2) (#) r) by Def6;
  now
    let k;
    assume
A37: k in dom r;
    then r/.k = r.k by PARTFUN1:def 6;
    then r/.k in C3 by A4,A37,FUNCT_1:def 3;
    then
A38: not r/.k in Carrier((L1 + L2)) by XBOOLE_0:def 5;
    k in dom((L1 + L2) (#) r) by A36,A37,FINSEQ_3:29;
    then ((L1 + L2) (#) r).k = (r/.k) * (L1 + L2).(r/.k) by Def6;
    hence ((L1 + L2) (#) r).k = (r/.k) * 0.R by A38;
  end;
  then
A39: Sum((L1 + L2) (#) r) = Sum(r) * 0.R by A36,Lm2
    .= 0.V by VECTSP_2:32;
A40: len p = len(L1 (#) p) by Def6;
  now
    let k;
    assume
A41: k in dom p;
    then p/.k = p.k by PARTFUN1:def 6;
    then p/.k in C1 by A1,A41,FUNCT_1:def 3;
    then
A42: not p/.k in Carrier(L1) by XBOOLE_0:def 5;
    k in dom(L1 (#) p) by A40,A41,FINSEQ_3:29;
    then (L1 (#) p).k = (p/.k) * L1.(p/.k) by Def6;
    hence (L1 (#) p).k = (p/.k) * 0.R by A42;
  end;
  then
A43: Sum(L1 (#) p) = Sum(p) * 0.R by A40,Lm2
    .= 0.V by VECTSP_2:32;
  set f = (L1 + L2) (#) FF;
  consider H such that
A44: H is one-to-one and
A45: rng H = Carrier(L2) and
A46: Sum(L2 (#) H) = Sum(L2) by Def7;
  set HH = H ^ q;
  rng H misses rng q
  proof
    set x = the Element of rng H /\ rng q;
    assume not thesis;
    then rng H /\ rng q <> {} by XBOOLE_0:def 7;
    then x in Carrier(L2) & x in C2 by A45,A7,XBOOLE_0:def 4;
    hence thesis by XBOOLE_0:def 5;
  end;
  then
A47: HH is one-to-one by A44,A8,FINSEQ_3:91;
A48: len q = len(L2 (#) q) by Def6;
  now
    let k;
    assume
A49: k in dom q;
    then q/.k = q.k by PARTFUN1:def 6;
    then q/.k in C2 by A7,A49,FUNCT_1:def 3;
    then
A50: not q/.k in Carrier(L2) by XBOOLE_0:def 5;
    k in dom(L2 (#) q) by A48,A49,FINSEQ_3:29;
    then (L2 (#) q).k = (q/.k) * L2.(q/.k) by Def6;
    hence (L2 (#) q).k = (q/.k) * 0.R by A50;
  end;
  then
A51: Sum(L2 (#) q) = Sum(q) * 0.R by A48,Lm2
    .= 0.V by VECTSP_2:32;
  set g = L1 (#) GG;
A52: len g = len GG by Def6;
  then
A53: Seg len GG = dom g by FINSEQ_1:def 3;
  rng HH = rng H \/ rng q by FINSEQ_1:31;
  then rng HH = Carrier(L2) \/ A by A45,A7,XBOOLE_1:39;
  then
A54: rng HH = A by XBOOLE_1:7,12;
  then
A55: len GG = len HH by A47,A18,A16,FINSEQ_1:48;
  deffunc Q(Nat)=HH <- (GG.$1);
  consider R being FinSequence such that
A56: len R = len HH and
A57: for k be Nat st k in dom R holds R.k = Q(k) from FINSEQ_1:sch 2;
A58: dom R = Seg len HH by A56,FINSEQ_1:def 3;
A59: now
    let x;
    assume
A60: x in dom GG;
    then reconsider n = x as Nat by FINSEQ_3:23;
    GG.n in rng HH by A16,A54,A60,FUNCT_1:def 3;
    then
A61: HH just_once_values GG.n by A47,FINSEQ_4:8;
    n in Seg(len HH) by A55,A60,FINSEQ_1:def 3;
    then HH.(R.n) = HH.(HH <- (GG.n)) by A57,A58
      .= GG.n by A61,FINSEQ_4:def 3;
    hence GG.x = HH.(R.x);
  end;
A62: dom GG = dom HH by A55,FINSEQ_3:29;
A63: rng R c= dom HH
  proof
    let x;
    assume x in rng R;
    then consider y such that
A64: y in dom R and
A65: R.y = x by FUNCT_1:def 3;
    reconsider y as Nat by A64,FINSEQ_3:23;
    y in dom HH by A56,A64,FINSEQ_3:29;
    then GG.y in rng HH by A16,A54,A62,FUNCT_1:def 3;
    then
A66: HH just_once_values GG.y by A47,FINSEQ_4:8;
    R.y = HH <- (GG.y) by A57,A64;
    hence thesis by A65,A66,FINSEQ_4:def 3;
  end;
  now
    let x;
    thus x in dom GG implies x in dom R & R.x in dom HH
    proof
      assume x in dom GG;
      then x in Seg(len R) by A55,A56,FINSEQ_1:def 3;
      hence x in dom R by FINSEQ_1:def 3;
      then R.x in rng R by FUNCT_1:def 3;
      hence thesis by A63;
    end;
    assume that
A67: x in dom R and
    R.x in dom HH;
    x in Seg(len R) by A67,FINSEQ_1:def 3;
    hence x in dom GG by A55,A56,FINSEQ_1:def 3;
  end;
  then
A68: GG = HH * R by A59,FUNCT_1:10;
  dom HH c= rng R
  proof
    set f = HH" * GG;
    let x;
    assume
A69: x in dom HH;
    dom(HH") = rng GG by A47,A16,A54,FUNCT_1:33;
    then
A70: rng f = rng(HH") by RELAT_1:28
      .= dom HH by A47,FUNCT_1:33;
    f = HH " * HH * R by A68,RELAT_1:36
      .= id(dom HH) * R by A47,FUNCT_1:39
      .= R by A63,RELAT_1:53;
    hence thesis by A69,A70;
  end;
  then
A71: dom HH = rng R by A63,XBOOLE_0:def 10;
A72: Sum(g) = Sum((L1 (#) G) ^ (L1 (#) p)) by Th28
    .= Sum(L1 (#) G) + 0.V by A43,RLVECT_1:41
    .= Sum(L1 (#) G) by RLVECT_1:def 4;
  set h = L2 (#) HH;
A73: Sum(h) = Sum((L2 (#) H) ^ (L2 (#) q)) by Th28
    .= Sum(L2 (#) H) + 0.V by A51,RLVECT_1:41
    .= Sum(L2 (#) H) by RLVECT_1:def 4;
A74: Sum(f) = Sum(((L1 + L2) (#) F) ^ ((L1 + L2) (#) r)) by Th28
    .= Sum((L1 + L2) (#) F) + 0.V by A39,RLVECT_1:41
    .= Sum((L1 + L2) (#) F) by RLVECT_1:def 4;
A75: dom P = dom FF by A20,FINSEQ_3:29;
  then
A76: P is one-to-one by A35,FINSEQ_4:60;
A77: dom R = dom HH by A56,FINSEQ_3:29;
  then
A78: R is one-to-one by A71,FINSEQ_4:60;
  reconsider R as Function of dom HH, dom HH by A63,A77,FUNCT_2:2
;
A79: len h = len HH by Def6;
  then
A80: dom h = dom HH by FINSEQ_3:29;
  then reconsider R as Function of dom h, dom h;
  reconsider Hp = h * R as FinSequence of V by FINSEQ_2:47;
  reconsider R as Permutation of dom h by A71,A78,A80,FUNCT_2:57;
A81: Hp = h * R;
  then
A82: len Hp = len GG by A55,A79,FINSEQ_2:44;
  reconsider P as Function of dom FF, dom FF by A27,A75,FUNCT_2:2
;
A83: len f = len FF by Def6;
  then
A84: dom f = dom FF by FINSEQ_3:29;
  then reconsider P as Function of dom f, dom f;
  reconsider Fp = f * P as FinSequence of V by FINSEQ_2:47;
  reconsider P as Permutation of dom f by A35,A76,A84,FUNCT_2:57;
A85: Fp = f * P;
  then
A86: Sum(Fp) = Sum(f) by RLVECT_2:7;
  deffunc Q(Nat) = (g/.$1) + (Hp/.$1);
  consider I being FinSequence such that
A87: len I = len GG and
A88: for k be Nat st k in dom I holds I.k = Q(k) from FINSEQ_1:sch 2;
A89: dom I = Seg len GG by A87,FINSEQ_1:def 3;
  then
A90: for k be Element of NAT st k in Seg(len GG) holds I.k = Q(k) by A88;
  rng I c= the carrier of V
  proof
    let x;
    assume x in rng I;
    then consider y such that
A91: y in dom I and
A92: I.y = x by FUNCT_1:def 3;
    reconsider y as Nat by A91,FINSEQ_3:23;
    I.y = (g/.y) + (Hp/.y) by A88,A91;
    hence thesis by A92;
  end;
  then reconsider I as FinSequence of V by FINSEQ_1:def 4;
A93: len Fp = len I by A19,A83,A85,A87,FINSEQ_2:44;
A94: now
    let x;
    assume
A95: x in Seg(len I);
    then reconsider k = x as Element of NAT;
A96: x in dom HH by A55,A87,A95,FINSEQ_1:def 3;
    then R.k in dom R by A71,A77,FUNCT_1:def 3;
    then reconsider j = R.k as Nat by FINSEQ_3:23;
A97: x in dom GG by A87,A95,FINSEQ_1:def 3;
    then
A98: HH.j = GG.k by A59
      .= GG/.k by A97,PARTFUN1:def 6;
    P.k in dom P by A26,A62,A35,A75,A96,FUNCT_1:def 3;
    then reconsider l = P.k as Nat by FINSEQ_3:23;
    set v = GG/.k;
A99: x in dom Fp by A93,A95,FINSEQ_1:def 3;
A100: FF.l = GG.k by A23,A97
      .= GG/.k by A97,PARTFUN1:def 6;
    P.k in dom FF by A26,A62,A35,A75,A96,FUNCT_1:def 3;
    then
A101: f.l = v * (L1 + L2).v by A100,Th23
      .= v * (L1.v + L2.v) by Def9
      .= v * L1.v + v * L2.v by VECTSP_2:def 9;
A102: x in dom Hp by A87,A82,A95,FINSEQ_1:def 3;
    then
A103: Hp/.k = (h * R).k by PARTFUN1:def 6
      .= h.(R.k) by A102,FUNCT_1:12;
    R.k in dom HH by A71,A77,A96,FUNCT_1:def 3;
    then
A104: h.j = v * L2.v by A98,Th23;
A105: x in dom g by A87,A52,A95,FINSEQ_1:def 3;
    then g/.k = g.k by PARTFUN1:def 6
      .= v * L1.v by A105,Def6;
    hence I.x = v * L1.v + v * L2.v by A87,A88,A89,A95,A103,A104
      .= Fp.x by A99,A101,FUNCT_1:12;
  end;
  dom I = Seg(len I) & dom Fp = Seg(len I) by A93,FINSEQ_1:def 3;
  then
A106: I = Fp by A94,FUNCT_1:2;
  Sum(Hp) = Sum(h) by A81,RLVECT_2:7;
  hence thesis by A11,A14,A46,A72,A73,A74,A86,A87,A90,A82,A52,A106,A53,
RLVECT_2:2;
end;

reserve R for domRing;
reserve V for RightMod of R;
reserve L,L1,L2 for Linear_Combination of V;
reserve a for Scalar of R;

theorem Th59:
  Sum(L * a) = Sum(L) * a
proof
  per cases;
  suppose
A1: a <> 0.R;
    set l = L * a;
A2: Carrier(l) = Carrier(L) by A1,Th43;
    consider G being FinSequence of V such that
A3: G is one-to-one and
A4: rng G = Carrier(L) and
A5: Sum(L) = Sum(L (#) G) by Def7;
    set g = L (#) G;
    consider F being FinSequence of V such that
A6: F is one-to-one and
A7: rng F = Carrier(L * a) and
A8: Sum(L * a) = Sum((L * a) (#) F) by Def7;
A9: len G = len F by A1,A6,A7,A3,A4,Th43,FINSEQ_1:48;
    set f = (L * a) (#) F;
    deffunc Q(Nat)= F <- (G.$1);
    consider P being FinSequence such that
A10: len P = len F and
A11: for k be Nat st k in dom P holds P.k = Q(k) from FINSEQ_1:sch 2;
A12: dom P = Seg len F by A10,FINSEQ_1:def 3;
A13: now
      let x;
      assume
A14:  x in dom G;
      then reconsider n = x as Nat by FINSEQ_3:23;
      G.n in rng F by A7,A4,A2,A14,FUNCT_1:def 3;
      then
A15:  F just_once_values G.n by A6,FINSEQ_4:8;
      n in Seg len F by A9,A14,FINSEQ_1:def 3;
      then F.(P.n) = F.(F <- (G.n)) by A11,A12
        .= G.n by A15,FINSEQ_4:def 3;
      hence G.x = F.(P.x);
    end;
A16: rng P c= dom F
    proof
      let x;
      assume x in rng P;
      then consider y such that
A17:  y in dom P and
A18:  P.y = x by FUNCT_1:def 3;
      reconsider y as Nat by A17,FINSEQ_3:23;
      y in dom G by A10,A9,A17,FINSEQ_3:29;
      then G.y in rng F by A7,A4,A2,FUNCT_1:def 3;
      then
A19:  F just_once_values G.y by A6,FINSEQ_4:8;
      P.y = F <- (G.y) by A11,A17;
      hence thesis by A18,A19,FINSEQ_4:def 3;
    end;
    now
      let x;
      thus x in dom G implies x in dom P & P.x in dom F
      proof
        assume x in dom G;
        then x in Seg(len P) by A10,A9,FINSEQ_1:def 3;
        hence x in dom P by FINSEQ_1:def 3;
        then P.x in rng P by FUNCT_1:def 3;
        hence thesis by A16;
      end;
      assume that
A20:  x in dom P and
      P.x in dom F;
      x in Seg(len P) by A20,FINSEQ_1:def 3;
      hence x in dom G by A10,A9,FINSEQ_1:def 3;
    end;
    then
A21: G = F * P by A13,FUNCT_1:10;
    dom F c= rng P
    proof
      set f = F" * G;
      let x;
      assume
A22:  x in dom F;
      dom(F") = rng G by A6,A7,A4,A2,FUNCT_1:33;
      then
A23:  rng f = rng(F") by RELAT_1:28
        .= dom F by A6,FUNCT_1:33;
      f = F " * F * P by A21,RELAT_1:36
        .= id(dom F) * P by A6,FUNCT_1:39
        .= P by A16,RELAT_1:53;
      hence thesis by A22,A23;
    end;
    then
A24: dom F = rng P by A16,XBOOLE_0:def 10;
A25: dom P = dom F by A10,FINSEQ_3:29;
    then
A26: P is one-to-one by A24,FINSEQ_4:60;
    reconsider P as Function of dom F, dom F by A16,A25,FUNCT_2:2
;
A27: len f = len F by Def6;
    then
A28: dom f = dom F by FINSEQ_3:29;
    then reconsider P as Function of dom f, dom f;
    reconsider Fp = f * P as FinSequence of V by FINSEQ_2:47;
    reconsider P as Permutation of dom f by A24,A26,A28,FUNCT_2:57;
A29: Fp = f * P;
    then
A30: len Fp = len f by FINSEQ_2:44;
    then
A31: len Fp = len g by A9,A27,Def6;
A32: now
      let k;
      let v be Vector of V;
      assume that
A33:  k in dom Fp and
A34:  v = g.k;
A35:  k in Seg(len g) by A31,A33,FINSEQ_1:def 3;
      then
A36:  k in dom P by A10,A27,A30,A31,FINSEQ_1:def 3;
A37:  k in dom G by A9,A27,A30,A31,A35,FINSEQ_1:def 3;
      then G.k in rng G by FUNCT_1:def 3;
      then F just_once_values G.k by A6,A7,A4,A2,FINSEQ_4:8;
      then
A38:  (F <- (G.k)) in dom F by FINSEQ_4:def 3;
      then reconsider i = F <- (G.k) as Nat by FINSEQ_3:23;
A39:  G/.k = G.k by A37,PARTFUN1:def 6
        .= F.(P.k) by A21,A36,FUNCT_1:13
        .= F.i by A11,A12,A27,A30,A31,A35
        .= F/.i by A38,PARTFUN1:def 6;
A40:  k in dom g by A35,FINSEQ_1:def 3;
      i in Seg(len f) by A27,A38,FINSEQ_1:def 3;
      then
A41:  i in dom f by FINSEQ_1:def 3;
      thus Fp.k = f.(P.k) by A36,FUNCT_1:13
        .= f.(F <- (G.k)) by A11,A12,A27,A30,A31,A35
        .= (F/.i) * l.(F/.i) by A41,Def6
        .= (F/.i) * (L.(F/.i) * a) by Def10
        .= (F/.i) * L.(F/.i) * a by VECTSP_2:def 9
        .= v * a by A34,A40,A39,Def6;
    end;
    Sum(Fp) = Sum(f) by A29,RLVECT_2:7;
    hence thesis by A8,A5,A31,A32,Th1;
  end;
  suppose
A42: a = 0.R;
    hence Sum(L * a) = Sum(ZeroLC(V)) by Th44
      .= 0.V by Lm3
      .= Sum(L) * a by A42,VECTSP_2:32;
  end;
end;

theorem Th60:
  Sum(- L) = - Sum(L)
proof
  thus Sum(- L) = Sum(L) * (- 1_R) by Th59
    .= - Sum(L) by VECTSP_2:32;
end;

theorem
  Sum(L1 - L2) = Sum(L1) - Sum(L2)
proof
  thus Sum(L1 - L2) = Sum(L1) + Sum(- L2) by Th58
    .= Sum(L1) + (- Sum(L2)) by Th60
    .= Sum(L1) - Sum(L2) by RLVECT_1:def 11;
end;

begin :: RMOD_5

reserve x for set;
reserve R for Ring;
reserve V for RightMod of R;
reserve v,v1,v2 for Vector of V;
reserve A,B for Subset of V;

definition
  let R, V;
  let IT be Subset of V;
  attr IT is linearly-independent means
  :Def13:
  for l being Linear_Combination of IT st Sum(l) = 0.V holds Carrier(l) = {};
end;

notation
  let R, V;
  let IT be Subset of V;
  antonym IT is linearly-dependent for IT is linearly-independent;
end;

theorem
  A c= B & B is linearly-independent implies A is linearly-independent
proof
  assume that
A1: A c= B and
A2: B is linearly-independent;
  let l be Linear_Combination of A;
  reconsider L = l as Linear_Combination of B by A1,Th19;
  assume Sum(l) = 0.V;
  then Carrier(L) = {} by A2,Def13;
  hence thesis;
end;

theorem Th63:
  0.R <> 1_R & A is linearly-independent implies not 0.V in A
proof
  assume that
A1: 0.R <> 1_R and
A2: A is linearly-independent and
A3: 0.V in A;
  deffunc F(Element of V)=0.R;
  consider f being Function of the carrier of V, the carrier of R such that
A4: f.(0.V) = 1_R and
A5: for v being Element of V st v <> 0.V holds f.v = F(v) from FUNCT_2:
  sch 6;
  reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
  ex T being finite Subset of V st for v st not v in T holds f.v = 0.R
  proof
    take T = {0.V};
    let v;
    assume not v in T;
    then v <> 0.V by TARSKI:def 1;
    hence thesis by A5;
  end;
  then reconsider f as Linear_Combination of V by Def2;
A6: Carrier(f) = {0.V}
  proof
    thus Carrier(f) c= {0.V}
    proof
      let x;
      assume x in Carrier(f);
      then consider v such that
A7:   v = x and
A8:   f.v <> 0.R;
      v = 0.V by A5,A8;
      hence thesis by A7,TARSKI:def 1;
    end;
    let x;
    assume x in {0.V};
    then x = 0.V by TARSKI:def 1;
    hence thesis by A1,A4;
  end;
  then Carrier(f) c= A by A3,ZFMISC_1:31;
  then reconsider f as Linear_Combination of A by Def5;
  Sum(f) = 0.V * f.(0.V) by A6,Th35
    .= 0.V by VECTSP_2:32;
  hence contradiction by A2,A6,Def13;
end;

theorem
  {}(the carrier of V) is linearly-independent
proof
  let l be Linear_Combination of {}(the carrier of V);
  Carrier(l) c= {} by Def5;
  hence thesis;
end;

theorem Th65:
  0.R <> 1_R & {v1,v2} is linearly-independent implies v1 <> 0.V & v2 <> 0.V
proof
A1: v1 in {v1,v2} & v2 in {v1,v2} by TARSKI:def 2;
  assume 0.R <> 1_R & {v1,v2} is linearly-independent;
  hence thesis by A1,Th63;
end;

theorem
  0.R <> 1_R implies {v,0.V} is linearly-dependent & {0.V,v} is
  linearly-dependent by Th65;

reserve R for domRing;
reserve V for RightMod of R;
reserve v,u for Vector of V;
reserve A,B for Subset of V;
reserve l for Linear_Combination of A;
reserve f,g for Function of the carrier of V, the carrier of R;

definition
  let R, V, A;
  func Lin(A) -> strict Submodule of V means
  :Def14:
  the carrier of it = {Sum( l) : not contradiction};
  existence
  proof
    set A1 = {Sum(l) : not contradiction};
    reconsider l = ZeroLC(V) as Linear_Combination of A by Th20;
    A1 c= the carrier of V
    proof
      let x;
      assume x in A1;
      then ex l st x = Sum(l);
      hence thesis;
    end;
    then reconsider A1 as Subset of V;
A1: A1 is linearly-closed
    proof
      thus for v,u st v in A1 & u in A1 holds v + u in A1
      proof
        let v,u;
        assume that
A2:     v in A1 and
A3:     u in A1;
        consider l1 being Linear_Combination of A such that
A4:     v = Sum(l1) by A2;
        consider l2 being Linear_Combination of A such that
A5:     u = Sum(l2) by A3;
        reconsider f = l1 + l2 as Linear_Combination of A by Th38;
        v + u = Sum(f) by A4,A5,Th58;
        hence thesis;
      end;
      let a be Scalar of R,v;
      assume v in A1;
      then consider l such that
A6:   v = Sum(l);
      reconsider f = l * a as Linear_Combination of A by Th45;
      v * a = Sum(f) by A6,Th59;
      hence thesis;
    end;
    Sum(l) = 0.V by Lm3;
    then 0.V in A1;
    hence thesis by A1,RMOD_2:34;
  end;
  uniqueness by RMOD_2:29;
end;

theorem Th67:
  x in Lin(A) iff ex l st x = Sum(l)
proof
  thus x in Lin(A) implies ex l st x = Sum(l)
  proof
    assume x in Lin(A);
    then x in the carrier of Lin(A) by STRUCT_0:def 5;
    then x in {Sum(l) : not contradiction} by Def14;
    hence thesis;
  end;
  given k being Linear_Combination of A such that
A1: x = Sum(k);
  x in {Sum(l): not contradiction} by A1;
  then x in the carrier of Lin(A) by Def14;
  hence thesis by STRUCT_0:def 5;
end;

theorem Th68:
  x in A implies x in Lin(A)
proof
  deffunc F(Element of V)=0.R;
  assume
A1: x in A;
  then reconsider v = x as Vector of V;
  consider f being Function of the carrier of V, the carrier of R such that
A2: f.v = 1_R and
A3: for u st u <> v holds f.u = F(u) from FUNCT_2:sch 6;
  reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
  ex T being finite Subset of V st for u st not u in T holds f.u = 0.R
  proof
    take T = {v};
    let u;
    assume not u in T;
    then u <> v by TARSKI:def 1;
    hence thesis by A3;
  end;
  then reconsider f as Linear_Combination of V by Def2;
A4: Carrier(f) c= {v}
  proof
    let x;
    assume x in Carrier(f);
    then consider u such that
A5: x = u and
A6: f.u <> 0.R;
    u = v by A3,A6;
    hence thesis by A5,TARSKI:def 1;
  end;
  then reconsider f as Linear_Combination of {v} by Def5;
A7: Sum(f) = v * 1_R by A2,Th32
    .= v by VECTSP_2:def 9;
  {v} c= A by A1,ZFMISC_1:31;
  then Carrier(f) c= A by A4,XBOOLE_1:1;
  then reconsider f as Linear_Combination of A by Def5;
  Sum(f) = v by A7;
  hence thesis by Th67;
end;

theorem
  Lin({}(the carrier of V)) = (0).V
proof
  set A = Lin({}(the carrier of V));
  now
    let v;
    thus v in A implies v in (0).V
    proof
      assume v in A;
      then
A1:   v in the carrier of A by STRUCT_0:def 5;
      the carrier of A = {Sum(l0) where l0 is Linear_Combination of {}(the
      carrier of V): not contradiction} by Def14;
      then
      ex l0 being Linear_Combination of {}(the carrier of V) st v = Sum(l0
      ) by A1;
      then v = 0.V by Th31;
      hence thesis by RMOD_2:35;
    end;
    assume v in (0).V;
    then v = 0.V by RMOD_2:35;
    hence v in A by RMOD_2:17;
  end;
  hence thesis by RMOD_2:30;
end;

theorem
  Lin(A) = (0).V implies A = {} or A = {0.V}
proof
  assume that
A1: Lin(A) = (0).V and
A2: A <> {};
  thus A c= {0.V}
  proof
    let x;
    assume x in A;
    then x in Lin(A) by Th68;
    then x = 0.V by A1,RMOD_2:35;
    hence thesis by TARSKI:def 1;
  end;
  set y = the Element of A;
  let x;
  assume x in {0.V};
  then
A3: x = 0.V by TARSKI:def 1;
  y in A & y in Lin(A) by A2,Th68;
  hence thesis by A1,A3,RMOD_2:35;
end;

theorem Th71:
  for W being strict Submodule of V st 0.R <> 1_R & A = the
  carrier of W holds Lin(A) = W
proof
  let W be strict Submodule of V;
  assume that
A1: 0.R <> 1_R and
A2: A = the carrier of W;
  now
    let v;
    thus v in Lin(A) implies v in W
    proof
      assume v in Lin(A);
      then
A3:   ex l st v = Sum(l) by Th67;
      A is linearly-closed by A2,RMOD_2:33;
      then v in the carrier of W by A1,A2,A3,Th29;
      hence thesis by STRUCT_0:def 5;
    end;
    v in W iff v in the carrier of W by STRUCT_0:def 5;
    hence v in W implies v in Lin(A) by A2,Th68;
  end;
  hence thesis by RMOD_2:30;
end;

theorem
  for V being strict RightMod of R, A being Subset of V st 0.R <> 1_R &
  A = the carrier of V holds Lin(A) = V
proof
  let V be strict RightMod of R, A be Subset of V such that
A1: 0.R <> 1_R;
  assume
A2: A = the carrier of V;
  (Omega).V = V;
  hence thesis by A1,A2,Th71;
end;

theorem Th73:
  A c= B implies Lin(A) is Submodule of Lin(B)
proof
  assume
A1: A c= B;
  now
    let v;
    assume v in Lin(A);
    then consider l such that
A2: v = Sum(l) by Th67;
    reconsider l as Linear_Combination of B by A1,Th19;
    Sum(l) = v by A2;
    hence v in Lin(B) by Th67;
  end;
  hence thesis by RMOD_2:28;
end;

theorem
  for V being strict RightMod of R, A,B being Subset of V st Lin(A) = V
  & A c= B holds Lin(B) = V
proof
  let V be strict RightMod of R, A,B be Subset of V;
  assume Lin(A) = V & A c= B;
  then V is Submodule of Lin(B) by Th73;
  hence thesis by RMOD_2:25;
end;

theorem
  Lin(A \/ B) = Lin(A) + Lin(B)
proof
  now
    deffunc G(set)=0.R;
    let v;
    assume v in Lin(A \/ B);
    then consider l being Linear_Combination of A \/ B such that
A1: v = Sum(l) by Th67;
    deffunc F(set)=l.$1;
    set D = Carrier(l) \ A;
    set C = Carrier(l) /\ A;
    defpred P[set] means $1 in C;
    defpred C[set] means $1 in D;
    now
      let x;
      assume x in the carrier of V;
      then reconsider v = x as Vector of V;
      f.v in the carrier of R;
      hence x in C implies l.x in the carrier of R;
      assume not x in C;
      thus 0.R in the carrier of R;
    end;
    then
A2: for x st x in the carrier of V holds (P[x] implies F(x) in the
    carrier of R ) & (not P[x] implies G(x) in the carrier of R);
    consider f being Function of the carrier of V, the carrier of R such that
A3: for x st x in the carrier of V holds (P[x] implies f.x = F(x)) &
    (not P[x] implies f.x = G(x)) from FUNCT_2:sch 5(A2);
    reconsider C as finite Subset of V;
    reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
    for u holds not u in C implies f.u = 0.R by A3;
    then reconsider f as Linear_Combination of V by Def2;
A4: Carrier(f) c= C
    proof
      let x;
      assume x in Carrier(f);
      then
A5:   ex u st x = u & f.u <> 0.R;
      assume not x in C;
      hence thesis by A3,A5;
    end;
    C c= A by XBOOLE_1:17;
    then Carrier(f) c= A by A4,XBOOLE_1:1;
    then reconsider f as Linear_Combination of A by Def5;
    now
      let x;
      assume x in the carrier of V;
      then reconsider v = x as Vector of V;
      g.v in the carrier of R;
      hence x in D implies l.x in the carrier of R;
      assume not x in D;
      thus 0.R in the carrier of R;
    end;
    then
A6: for x st x in the carrier of V holds (C[x] implies F(x) in the
    carrier of R) & (not C[x] implies G(x) in the carrier of R);
    consider g being Function of the carrier of V, the carrier of R such that
A7: for x st x in the carrier of V holds (C[x] implies g.x = F(x)) &
    (not C[x] implies g.x = G(x)) from FUNCT_2:sch 5(A6);
    reconsider D as finite Subset of V;
    reconsider g as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
    for u holds not u in D implies g.u = 0.R by A7;
    then reconsider g as Linear_Combination of V by Def2;
A8: D c= B
    proof
      let x;
      assume x in D;
      then
A9:   x in Carrier(l) & not x in A by XBOOLE_0:def 5;
      Carrier(l) c= A \/ B by Def5;
      hence thesis by A9,XBOOLE_0:def 3;
    end;
    Carrier(g) c= D
    proof
      let x;
      assume x in Carrier(g);
      then
A10:  ex u st x = u & g.u <> 0.R;
      assume not x in D;
      hence thesis by A7,A10;
    end;
    then Carrier(g) c= B by A8,XBOOLE_1:1;
    then reconsider g as Linear_Combination of B by Def5;
    l = f + g
    proof
      let v;
      now
        per cases;
        suppose
A11:      v in C;
A12:      now
            assume v in D;
            then not v in A by XBOOLE_0:def 5;
            hence contradiction by A11,XBOOLE_0:def 4;
          end;
          thus (f + g).v = f.v + g.v by Def9
            .= l.v + g.v by A3,A11
            .= l.v + 0.R by A7,A12
            .= l.v by RLVECT_1:4;
        end;
        suppose
A13:      not v in C;
          now
            per cases;
            suppose
A14:          v in Carrier(l);
A15:          now
                assume not v in D;
                then not v in Carrier(l) or v in A by XBOOLE_0:def 5;
                hence contradiction by A13,A14,XBOOLE_0:def 4;
              end;
              thus (f + g). v = f.v + g.v by Def9
                .= 0.R + g.v by A3,A13
                .= g.v by RLVECT_1:4
                .= l.v by A7,A15;
            end;
            suppose
A16:          not v in Carrier(l);
              then
A17:          not v in D by XBOOLE_0:def 5;
A18:          not v in C by A16,XBOOLE_0:def 4;
              thus (f + g).v = f.v + g.v by Def9
                .= 0.R + g.v by A3,A18
                .= 0.R + 0.R by A7,A17
                .= 0.R by RLVECT_1:4
                .= l.v by A16;
            end;
          end;
          hence thesis;
        end;
      end;
      hence thesis;
    end;
    then
A19: v = Sum(f) + Sum(g) by A1,Th58;
    Sum(f) in Lin(A) & Sum(g) in Lin(B) by Th67;
    hence v in Lin(A) + Lin(B) by A19,RMOD_3:1;
  end;
  then
A20: Lin(A \/ B) is Submodule of Lin(A) + Lin(B) by RMOD_2:28;
  Lin(A) is Submodule of Lin(A \/ B) & Lin(B) is Submodule of Lin(A \/ B)
  by Th73,XBOOLE_1:7;
  then Lin(A) + Lin(B) is Submodule of Lin(A \/ B) by RMOD_3:35;
  hence thesis by A20,RMOD_2:25;
end;

theorem
  Lin(A /\ B) is Submodule of Lin(A) /\ Lin(B)
proof
  Lin(A /\ B) is Submodule of Lin(A) & Lin(A /\ B) is Submodule of Lin(B)
  by Th73,XBOOLE_1:17;
  hence thesis by RMOD_3:20;
end;