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 * (canFS A) & l2 = l * (canFS B) 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 * (canFS A) & l2 = l * (canFS B) 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 * (canFS A) & l2 = l * (canFS B) 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 * (canFS A) & l2 = l * (canFS B) 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 * (canFS A) & l2 = l * (canFS B) implies Sum l0 = (Sum l1) + (Sum l2) )

assume A1: A /\ B = {} ; :: thesis: ( not l0 = l * (canFS (A \/ B)) or not l1 = l * (canFS A) or not l2 = l * (canFS B) or Sum l0 = (Sum l1) + (Sum l2) )

assume TT: ( l0 = l * (canFS (A \/ B)) & l1 = l * (canFS A) & l2 = l * (canFS B) ) ; :: thesis: Sum l0 = (Sum l1) + (Sum l2)

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 * (canFS A) & l2 = l * (canFS B) 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 * (canFS A) & l2 = l * (canFS B) 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 * (canFS A) & l2 = l * (canFS B) 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 * (canFS A) & l2 = l * (canFS B) 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 * (canFS A) & l2 = l * (canFS B) implies Sum l0 = (Sum l1) + (Sum l2) )

assume A1: A /\ B = {} ; :: thesis: ( not l0 = l * (canFS (A \/ B)) or not l1 = l * (canFS A) or not l2 = l * (canFS B) or Sum l0 = (Sum l1) + (Sum l2) )

assume TT: ( l0 = l * (canFS (A \/ B)) & l1 = l * (canFS A) & l2 = l * (canFS B) ) ; :: thesis: Sum l0 = (Sum l1) + (Sum l2)

per cases
( A \/ B = {} or A \/ B <> {} )
;

end;

suppose A2:
A \/ B = {}
; :: thesis: Sum l0 = (Sum l1) + (Sum l2)

then A3:
A = {}
;

a3: B = {} by A2;

rng (l * (canFS B)) c= the carrier of R ;

then reconsider lC = l * (canFS B) 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;a3: B = {} by A2;

rng (l * (canFS B)) c= the carrier of R ;

then reconsider lC = l * (canFS B) 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

suppose A5:
A \/ B <> {}
; :: thesis: Sum l0 = (Sum l1) + (Sum l2)

rng (canFS A) = A
by FUNCT_2:def 3;

then reconsider ca = canFS A as the carrier of V -valued FinSequence by RELAT_1:def 19;

rng (canFS B) = 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 (canFS A);

set lb = len (canFS B);

set lab = len ((canFS A) ^ (canFS B));

set lavb = len (canFS (A \/ B));

set F = l * (canFS (A \/ B));

set G = l1 ^ l2;

set H = ((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B));

A6: len (canFS A) = card A by FINSEQ_1:93;

A7: len (canFS (A \/ B)) = card (A \/ B) by FINSEQ_1:93

.= (card A) + (card B) by A1, CARD_2:40, XBOOLE_0:def 7

.= (len (canFS A)) + (len (canFS B)) by A6, FINSEQ_1:93 ;

A8: len ((canFS A) ^ (canFS B)) = (len (canFS A)) + (len (canFS B)) by FINSEQ_1:22;

then A9: dom ((canFS A) ^ (canFS B)) = Seg ((len (canFS A)) + (len (canFS B))) by FINSEQ_1:def 3;

A10: rng ((canFS A) ^ (canFS B)) = (rng (canFS A)) \/ (rng (canFS B)) by FINSEQ_1:31

.= A \/ (rng (canFS B)) by FUNCT_2:def 3

.= A \/ B by FUNCT_2:def 3 ;

reconsider AB = (canFS A) ^ (canFS B) as Function of (Seg ((len (canFS A)) + (len (canFS B)))),(A \/ B) by A9, A10, FUNCT_2:1;

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 A11, FUNCT_2:1;

A15: dom INVAB = A \/ B by A5, FUNCT_2:def 1;

A16: rng INVAB = Seg (card (A \/ B)) by A12, A13, A14, FUNCT_2:18

.= Seg ((card A) + (card B)) by A1, CARD_2:40, XBOOLE_0:def 7

.= Seg ((len (canFS A)) + (len (canFS B))) by A6, FINSEQ_1:93 ;

A17: dom (((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B))) = dom ((canFS A) ^ (canFS B)) by A10, A15, RELAT_1:27

.= Seg ((len (canFS A)) + (len (canFS B))) by A8, FINSEQ_1:def 3 ;

A18: rng (((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B))) = Seg ((len (canFS A)) + (len (canFS B))) by A10, A15, A16, RELAT_1:28;

A19: the carrier of V = dom l by FUNCT_2:def 1;

A20: dom (l * (canFS (A \/ B))) = dom (canFS (A \/ B)) by A11, A19, RELAT_1:27

.= Seg ((len (canFS A)) + (len (canFS B))) by A7, FINSEQ_1:def 3 ;

rng (canFS A) = A by FUNCT_2:def 3;

then dom (l * (canFS A)) = dom (canFS A) by A19, RELAT_1:27

.= Seg (len (canFS A)) by FINSEQ_1:def 3 ;

then A21: len (l * (canFS A)) = len (canFS A) by FINSEQ_1:def 3;

A22: rng (canFS B) = B by FUNCT_2:def 3;

then dom (l * (canFS B)) = dom (canFS B) by A19, RELAT_1:27

.= Seg (len (canFS B)) by FINSEQ_1:def 3 ;

then A23: len (l * (canFS B)) = len (canFS B) by FINSEQ_1:def 3;

set G = (l * (canFS A)) ^ (l * (canFS B));

A24: len ((l * (canFS A)) ^ (l * (canFS B))) = (len (canFS A)) + (len (canFS B)) by A21, A23, FINSEQ_1:22;

rng (canFS A) misses rng (canFS B) by A1, A22, FUNCT_2:def 3;

then A25: (canFS A) ^ (canFS B) is one-to-one by FINSEQ_3:91;

A26: dom (((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B))) = dom ((l * (canFS A)) ^ (l * (canFS B))) by A17, A24, FINSEQ_1:def 3;

A27: (l * (canFS (A \/ B))) * (((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B))) = ((l * (canFS (A \/ B))) * ((canFS (A \/ B)) ")) * ((canFS A) ^ (canFS B)) by RELAT_1:36

.= (l * ((canFS (A \/ B)) * ((canFS (A \/ B)) "))) * ((canFS A) ^ (canFS B)) by RELAT_1:36

.= (l * (id (rng (canFS (A \/ B))))) * ((canFS A) ^ (canFS B)) by FUNCT_1:39

.= (l * (id (A \/ B))) * ((canFS A) ^ (canFS B)) by FUNCT_2:def 3

.= l * ((id (A \/ B)) * AB) by RELAT_1:36

.= l * ((canFS A) ^ (canFS B)) by FUNCT_2:17

.= (l * ca) ^ (l * cb) by ThTF3C3

.= (l * (canFS A)) ^ (l * (canFS B)) ;

Z2: rng ((l * (canFS A)) ^ (l * (canFS B))) = (rng (l * (canFS A))) \/ (rng (l * (canFS B))) 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 * (canFS A)) ^ (l * (canFS B)) as FinSequence of R by Z2, FINSEQ_1:def 4;

thus Sum l0 = Sum FR by TT

.= Sum GR by A18, A20, A25, A26, A27, CLASSES1:77, RF9

.= Sum (l1 ^ l2) by TT

.= (Sum (l * (canFS A))) + (Sum (l * (canFS B))) by TT, RLVECT_1:41

.= (Sum l1) + (Sum l2) by TT ; :: thesis: verum

end;then reconsider ca = canFS A as the carrier of V -valued FinSequence by RELAT_1:def 19;

rng (canFS B) = 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 (canFS A);

set lb = len (canFS B);

set lab = len ((canFS A) ^ (canFS B));

set lavb = len (canFS (A \/ B));

set F = l * (canFS (A \/ B));

set G = l1 ^ l2;

set H = ((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B));

A6: len (canFS A) = card A by FINSEQ_1:93;

A7: len (canFS (A \/ B)) = card (A \/ B) by FINSEQ_1:93

.= (card A) + (card B) by A1, CARD_2:40, XBOOLE_0:def 7

.= (len (canFS A)) + (len (canFS B)) by A6, FINSEQ_1:93 ;

A8: len ((canFS A) ^ (canFS B)) = (len (canFS A)) + (len (canFS B)) by FINSEQ_1:22;

then A9: dom ((canFS A) ^ (canFS B)) = Seg ((len (canFS A)) + (len (canFS B))) by FINSEQ_1:def 3;

A10: rng ((canFS A) ^ (canFS B)) = (rng (canFS A)) \/ (rng (canFS B)) by FINSEQ_1:31

.= A \/ (rng (canFS B)) by FUNCT_2:def 3

.= A \/ B by FUNCT_2:def 3 ;

reconsider AB = (canFS A) ^ (canFS B) as Function of (Seg ((len (canFS A)) + (len (canFS B)))),(A \/ B) by A9, A10, FUNCT_2:1;

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 A11, FUNCT_2:1;

A15: dom INVAB = A \/ B by A5, FUNCT_2:def 1;

A16: rng INVAB = Seg (card (A \/ B)) by A12, A13, A14, FUNCT_2:18

.= Seg ((card A) + (card B)) by A1, CARD_2:40, XBOOLE_0:def 7

.= Seg ((len (canFS A)) + (len (canFS B))) by A6, FINSEQ_1:93 ;

A17: dom (((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B))) = dom ((canFS A) ^ (canFS B)) by A10, A15, RELAT_1:27

.= Seg ((len (canFS A)) + (len (canFS B))) by A8, FINSEQ_1:def 3 ;

A18: rng (((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B))) = Seg ((len (canFS A)) + (len (canFS B))) by A10, A15, A16, RELAT_1:28;

A19: the carrier of V = dom l by FUNCT_2:def 1;

A20: dom (l * (canFS (A \/ B))) = dom (canFS (A \/ B)) by A11, A19, RELAT_1:27

.= Seg ((len (canFS A)) + (len (canFS B))) by A7, FINSEQ_1:def 3 ;

rng (canFS A) = A by FUNCT_2:def 3;

then dom (l * (canFS A)) = dom (canFS A) by A19, RELAT_1:27

.= Seg (len (canFS A)) by FINSEQ_1:def 3 ;

then A21: len (l * (canFS A)) = len (canFS A) by FINSEQ_1:def 3;

A22: rng (canFS B) = B by FUNCT_2:def 3;

then dom (l * (canFS B)) = dom (canFS B) by A19, RELAT_1:27

.= Seg (len (canFS B)) by FINSEQ_1:def 3 ;

then A23: len (l * (canFS B)) = len (canFS B) by FINSEQ_1:def 3;

set G = (l * (canFS A)) ^ (l * (canFS B));

A24: len ((l * (canFS A)) ^ (l * (canFS B))) = (len (canFS A)) + (len (canFS B)) by A21, A23, FINSEQ_1:22;

rng (canFS A) misses rng (canFS B) by A1, A22, FUNCT_2:def 3;

then A25: (canFS A) ^ (canFS B) is one-to-one by FINSEQ_3:91;

A26: dom (((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B))) = dom ((l * (canFS A)) ^ (l * (canFS B))) by A17, A24, FINSEQ_1:def 3;

A27: (l * (canFS (A \/ B))) * (((canFS (A \/ B)) ") * ((canFS A) ^ (canFS B))) = ((l * (canFS (A \/ B))) * ((canFS (A \/ B)) ")) * ((canFS A) ^ (canFS B)) by RELAT_1:36

.= (l * ((canFS (A \/ B)) * ((canFS (A \/ B)) "))) * ((canFS A) ^ (canFS B)) by RELAT_1:36

.= (l * (id (rng (canFS (A \/ B))))) * ((canFS A) ^ (canFS B)) by FUNCT_1:39

.= (l * (id (A \/ B))) * ((canFS A) ^ (canFS B)) by FUNCT_2:def 3

.= l * ((id (A \/ B)) * AB) by RELAT_1:36

.= l * ((canFS A) ^ (canFS B)) by FUNCT_2:17

.= (l * ca) ^ (l * cb) by ThTF3C3

.= (l * (canFS A)) ^ (l * (canFS B)) ;

Z2: rng ((l * (canFS A)) ^ (l * (canFS B))) = (rng (l * (canFS A))) \/ (rng (l * (canFS B))) 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 * (canFS A)) ^ (l * (canFS B)) as FinSequence of R by Z2, FINSEQ_1:def 4;

thus Sum l0 = Sum FR by TT

.= Sum GR by A18, A20, A25, A26, A27, CLASSES1:77, RF9

.= Sum (l1 ^ l2) by TT

.= (Sum (l * (canFS A))) + (Sum (l * (canFS B))) by TT, RLVECT_1:41

.= (Sum l1) + (Sum l2) by TT ; :: thesis: verum