let R be Ring; :: thesis: for V being LeftMod of R
for A, B being finite Subset of V
for l being Linear_Combination of V
for l0, l1, l2 being FinSequence of R st A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * () & l2 = l * () holds
Sum l0 = (Sum l1) + (Sum l2)

let V be LeftMod of R; :: thesis: for A, B being finite Subset of V
for l being Linear_Combination of V
for l0, l1, l2 being FinSequence of R st A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * () & l2 = l * () holds
Sum l0 = (Sum l1) + (Sum l2)

let A, B be finite Subset of V; :: thesis: for l being Linear_Combination of V
for l0, l1, l2 being FinSequence of R st A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * () & l2 = l * () holds
Sum l0 = (Sum l1) + (Sum l2)

let l be Linear_Combination of V; :: thesis: for l0, l1, l2 being FinSequence of R st A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * () & l2 = l * () holds
Sum l0 = (Sum l1) + (Sum l2)

let l0, l1, l2 be FinSequence of R; :: thesis: ( A /\ B = {} & l0 = l * (canFS (A \/ B)) & l1 = l * () & l2 = l * () implies Sum l0 = (Sum l1) + (Sum l2) )
assume A1: A /\ B = {} ; :: thesis: ( not l0 = l * (canFS (A \/ B)) or not l1 = l * () or not l2 = l * () or Sum l0 = (Sum l1) + (Sum l2) )
assume TT: ( l0 = l * (canFS (A \/ B)) & l1 = l * () & l2 = l * () ) ; :: thesis: Sum l0 = (Sum l1) + (Sum l2)
per cases ( A \/ B = {} or A \/ B <> {} ) ;
suppose A2: A \/ B = {} ; :: thesis: Sum l0 = (Sum l1) + (Sum l2)
then A3: A = {} ;
a3: B = {} by A2;
rng (l * ()) c= the carrier of R ;
then reconsider lC = l * () as FinSequence of R by FINSEQ_1:def 4;
lC = <*> the carrier of R by a3;
then Sum lC = 0. R by RLVECT_1:43
.= 0. R ;
hence Sum l0 = (Sum l1) + (Sum l2) by A2, A3, TT; :: thesis: verum
end;
suppose A5: A \/ B <> {} ; :: thesis: Sum l0 = (Sum l1) + (Sum l2)
rng () = A by FUNCT_2:def 3;
then reconsider ca = canFS A as the carrier of V -valued FinSequence by RELAT_1:def 19;
rng () = B by FUNCT_2:def 3;
then reconsider cb = canFS B as the carrier of V -valued FinSequence by RELAT_1:def 19;
set la = len ();
set lb = len ();
set lab = len (() ^ ());
set lavb = len (canFS (A \/ B));
set F = l * (canFS (A \/ B));
set G = l1 ^ l2;
set H = ((canFS (A \/ B)) ") * (() ^ ());
A6: len () = card A by FINSEQ_1:93;
A7: len (canFS (A \/ B)) = card (A \/ B) by FINSEQ_1:93
.= (card A) + (card B) by
.= (len ()) + (len ()) by ;
A8: len (() ^ ()) = (len ()) + (len ()) by FINSEQ_1:22;
then A9: dom (() ^ ()) = Seg ((len ()) + (len ())) by FINSEQ_1:def 3;
A10: rng (() ^ ()) = (rng ()) \/ (rng ()) by FINSEQ_1:31
.= A \/ (rng ()) by FUNCT_2:def 3
.= A \/ B by FUNCT_2:def 3 ;
reconsider AB = () ^ () as Function of (Seg ((len ()) + (len ()))),(A \/ B) by ;
A11: rng (canFS (A \/ B)) = A \/ B by FUNCT_2:def 3;
reconsider INVAB = (canFS (A \/ B)) " as Function of (A \/ B),(Seg (card (A \/ B))) by FINSEQ_1:95;
A12: ( INVAB * (canFS (A \/ B)) = id (dom (canFS (A \/ B))) & (canFS (A \/ B)) * INVAB = id (rng (canFS (A \/ B))) ) by FUNCT_1:39;
A13: dom (canFS (A \/ B)) = Seg (len (canFS (A \/ B))) by FINSEQ_1:def 3
.= Seg (card (A \/ B)) by FINSEQ_1:93 ;
then A14: canFS (A \/ B) is Function of (Seg (card (A \/ B))),(A \/ B) by ;
A15: dom INVAB = A \/ B by ;
A16: rng INVAB = Seg (card (A \/ B)) by
.= Seg ((card A) + (card B)) by
.= Seg ((len ()) + (len ())) by ;
A17: dom (((canFS (A \/ B)) ") * (() ^ ())) = dom (() ^ ()) by
.= Seg ((len ()) + (len ())) by ;
A18: rng (((canFS (A \/ B)) ") * (() ^ ())) = Seg ((len ()) + (len ())) by ;
A19: the carrier of V = dom l by FUNCT_2:def 1;
A20: dom (l * (canFS (A \/ B))) = dom (canFS (A \/ B)) by
.= Seg ((len ()) + (len ())) by ;
rng () = A by FUNCT_2:def 3;
then dom (l * ()) = dom () by
.= Seg (len ()) by FINSEQ_1:def 3 ;
then A21: len (l * ()) = len () by FINSEQ_1:def 3;
A22: rng () = B by FUNCT_2:def 3;
then dom (l * ()) = dom () by
.= Seg (len ()) by FINSEQ_1:def 3 ;
then A23: len (l * ()) = len () by FINSEQ_1:def 3;
set G = (l * ()) ^ (l * ());
A24: len ((l * ()) ^ (l * ())) = (len ()) + (len ()) by ;
rng () misses rng () by ;
then A25: (canFS A) ^ () is one-to-one by FINSEQ_3:91;
A26: dom (((canFS (A \/ B)) ") * (() ^ ())) = dom ((l * ()) ^ (l * ())) by ;
A27: (l * (canFS (A \/ B))) * (((canFS (A \/ B)) ") * (() ^ ())) = ((l * (canFS (A \/ B))) * ((canFS (A \/ B)) ")) * (() ^ ()) by RELAT_1:36
.= (l * ((canFS (A \/ B)) * ((canFS (A \/ B)) "))) * (() ^ ()) by RELAT_1:36
.= (l * (id (rng (canFS (A \/ B))))) * (() ^ ()) by FUNCT_1:39
.= (l * (id (A \/ B))) * (() ^ ()) by FUNCT_2:def 3
.= l * ((id (A \/ B)) * AB) by RELAT_1:36
.= l * (() ^ ()) by FUNCT_2:17
.= (l * ca) ^ (l * cb) by ThTF3C3
.= (l * ()) ^ (l * ()) ;
Z2: rng ((l * ()) ^ (l * ())) = (rng (l * ())) \/ (rng (l * ())) by FINSEQ_1:31;
rng (l * (canFS (A \/ B))) c= the carrier of R ;
then reconsider FR = l * (canFS (A \/ B)) as FinSequence of R by FINSEQ_1:def 4;
reconsider GR = (l * ()) ^ (l * ()) as FinSequence of R by ;
thus Sum l0 = Sum FR by TT
.= Sum GR by
.= Sum (l1 ^ l2) by TT
.= (Sum (l * ())) + (Sum (l * ())) by
.= (Sum l1) + (Sum l2) by TT ; :: thesis: verum
end;
end;