let S be non empty addLoopStr ; :: thesis: for LS1, LS2 being Linear_Combination of S holds sum (LS1 + LS2) = (sum LS1) + (sum LS2)

let LS1, LS2 be Linear_Combination of S; :: thesis: sum (LS1 + LS2) = (sum LS1) + (sum LS2)

set C1 = Carrier LS1;

set C2 = Carrier LS2;

consider p112 being FinSequence such that

A1: rng p112 = (Carrier LS1) \ (Carrier LS2) and

A2: p112 is one-to-one by FINSEQ_4:58;

consider p12 being FinSequence such that

A3: rng p12 = (Carrier LS1) /\ (Carrier LS2) and

A4: p12 is one-to-one by FINSEQ_4:58;

consider p211 being FinSequence such that

A5: rng p211 = (Carrier LS2) \ (Carrier LS1) and

A6: p211 is one-to-one by FINSEQ_4:58;

reconsider p112 = p112, p12 = p12, p211 = p211 as FinSequence of S by A1, A3, A5, FINSEQ_1:def 4;

(Carrier LS1) \ (Carrier LS2) misses (Carrier LS1) /\ (Carrier LS2) by XBOOLE_1:89;

then A7: p112 ^ p12 is one-to-one by A1, A2, A3, A4, FINSEQ_3:91;

set p1 = p112 ^ p12;

A8: rng (p112 ^ p12) = ((Carrier LS1) \ (Carrier LS2)) \/ ((Carrier LS1) /\ (Carrier LS2)) by A1, A3, FINSEQ_1:31

.= Carrier LS1 by XBOOLE_1:51 ;

then A9: rng ((p112 ^ p12) ^ p211) = (Carrier LS1) \/ ((Carrier LS2) \ (Carrier LS1)) by A5, FINSEQ_1:31

.= (Carrier LS1) \/ (Carrier LS2) by XBOOLE_1:39 ;

set p2 = p12 ^ p211;

A10: rng (p12 ^ p211) = ((Carrier LS1) /\ (Carrier LS2)) \/ ((Carrier LS2) \ (Carrier LS1)) by A3, A5, FINSEQ_1:31

.= Carrier LS2 by XBOOLE_1:51 ;

set pp = (p112 ^ p12) ^ p211;

(p112 ^ p12) ^ p211 = p112 ^ (p12 ^ p211) by FINSEQ_1:32;

then A11: LS2 * ((p112 ^ p12) ^ p211) = (LS2 * p112) ^ (LS2 * (p12 ^ p211)) by FINSEQOP:9;

(Carrier LS2) \ (Carrier LS1) misses (Carrier LS1) /\ (Carrier LS2) by XBOOLE_1:89;

then A12: p12 ^ p211 is one-to-one by A3, A4, A5, A6, FINSEQ_3:91;

Carrier LS2 misses (Carrier LS1) \ (Carrier LS2) by XBOOLE_1:79;

then Sum (LS2 * p112) = 0 by A1, Th29;

then A13: Sum (LS2 * ((p112 ^ p12) ^ p211)) = 0 + (Sum (LS2 * (p12 ^ p211))) by A11, RVSUM_1:75

.= sum LS2 by A10, A12, Def3 ;

( len (LS1 * ((p112 ^ p12) ^ p211)) = len ((p112 ^ p12) ^ p211) & len (LS2 * ((p112 ^ p12) ^ p211)) = len ((p112 ^ p12) ^ p211) ) by FINSEQ_2:33;

then reconsider L1p = LS1 * ((p112 ^ p12) ^ p211), L2p = LS2 * ((p112 ^ p12) ^ p211) as Element of (len ((p112 ^ p12) ^ p211)) -tuples_on REAL by FINSEQ_2:92;

A14: (LS1 + LS2) * ((p112 ^ p12) ^ p211) = L1p + L2p by Th13;

A15: Carrier LS1 misses (Carrier LS2) \ (Carrier LS1) by XBOOLE_1:79;

then ( LS1 * ((p112 ^ p12) ^ p211) = (LS1 * (p112 ^ p12)) ^ (LS1 * p211) & Sum (LS1 * p211) = 0 ) by A5, Th29, FINSEQOP:9;

then A16: Sum (LS1 * ((p112 ^ p12) ^ p211)) = (Sum (LS1 * (p112 ^ p12))) + 0 by RVSUM_1:75

.= sum LS1 by A7, A8, Def3 ;

A17: Carrier (LS1 + LS2) c= (Carrier LS1) \/ (Carrier LS2)

hence sum (LS1 + LS2) = Sum (L1p + L2p) by A9, A14, A17, Th30

.= (sum LS1) + (sum LS2) by A13, A16, RVSUM_1:89 ;

:: thesis: verum

let LS1, LS2 be Linear_Combination of S; :: thesis: sum (LS1 + LS2) = (sum LS1) + (sum LS2)

set C1 = Carrier LS1;

set C2 = Carrier LS2;

consider p112 being FinSequence such that

A1: rng p112 = (Carrier LS1) \ (Carrier LS2) and

A2: p112 is one-to-one by FINSEQ_4:58;

consider p12 being FinSequence such that

A3: rng p12 = (Carrier LS1) /\ (Carrier LS2) and

A4: p12 is one-to-one by FINSEQ_4:58;

consider p211 being FinSequence such that

A5: rng p211 = (Carrier LS2) \ (Carrier LS1) and

A6: p211 is one-to-one by FINSEQ_4:58;

reconsider p112 = p112, p12 = p12, p211 = p211 as FinSequence of S by A1, A3, A5, FINSEQ_1:def 4;

(Carrier LS1) \ (Carrier LS2) misses (Carrier LS1) /\ (Carrier LS2) by XBOOLE_1:89;

then A7: p112 ^ p12 is one-to-one by A1, A2, A3, A4, FINSEQ_3:91;

set p1 = p112 ^ p12;

A8: rng (p112 ^ p12) = ((Carrier LS1) \ (Carrier LS2)) \/ ((Carrier LS1) /\ (Carrier LS2)) by A1, A3, FINSEQ_1:31

.= Carrier LS1 by XBOOLE_1:51 ;

then A9: rng ((p112 ^ p12) ^ p211) = (Carrier LS1) \/ ((Carrier LS2) \ (Carrier LS1)) by A5, FINSEQ_1:31

.= (Carrier LS1) \/ (Carrier LS2) by XBOOLE_1:39 ;

set p2 = p12 ^ p211;

A10: rng (p12 ^ p211) = ((Carrier LS1) /\ (Carrier LS2)) \/ ((Carrier LS2) \ (Carrier LS1)) by A3, A5, FINSEQ_1:31

.= Carrier LS2 by XBOOLE_1:51 ;

set pp = (p112 ^ p12) ^ p211;

(p112 ^ p12) ^ p211 = p112 ^ (p12 ^ p211) by FINSEQ_1:32;

then A11: LS2 * ((p112 ^ p12) ^ p211) = (LS2 * p112) ^ (LS2 * (p12 ^ p211)) by FINSEQOP:9;

(Carrier LS2) \ (Carrier LS1) misses (Carrier LS1) /\ (Carrier LS2) by XBOOLE_1:89;

then A12: p12 ^ p211 is one-to-one by A3, A4, A5, A6, FINSEQ_3:91;

Carrier LS2 misses (Carrier LS1) \ (Carrier LS2) by XBOOLE_1:79;

then Sum (LS2 * p112) = 0 by A1, Th29;

then A13: Sum (LS2 * ((p112 ^ p12) ^ p211)) = 0 + (Sum (LS2 * (p12 ^ p211))) by A11, RVSUM_1:75

.= sum LS2 by A10, A12, Def3 ;

( len (LS1 * ((p112 ^ p12) ^ p211)) = len ((p112 ^ p12) ^ p211) & len (LS2 * ((p112 ^ p12) ^ p211)) = len ((p112 ^ p12) ^ p211) ) by FINSEQ_2:33;

then reconsider L1p = LS1 * ((p112 ^ p12) ^ p211), L2p = LS2 * ((p112 ^ p12) ^ p211) as Element of (len ((p112 ^ p12) ^ p211)) -tuples_on REAL by FINSEQ_2:92;

A14: (LS1 + LS2) * ((p112 ^ p12) ^ p211) = L1p + L2p by Th13;

A15: Carrier LS1 misses (Carrier LS2) \ (Carrier LS1) by XBOOLE_1:79;

then ( LS1 * ((p112 ^ p12) ^ p211) = (LS1 * (p112 ^ p12)) ^ (LS1 * p211) & Sum (LS1 * p211) = 0 ) by A5, Th29, FINSEQOP:9;

then A16: Sum (LS1 * ((p112 ^ p12) ^ p211)) = (Sum (LS1 * (p112 ^ p12))) + 0 by RVSUM_1:75

.= sum LS1 by A7, A8, Def3 ;

A17: Carrier (LS1 + LS2) c= (Carrier LS1) \/ (Carrier LS2)

proof

(p112 ^ p12) ^ p211 is one-to-one
by A5, A6, A7, A8, A15, FINSEQ_3:91;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier (LS1 + LS2) or x in (Carrier LS1) \/ (Carrier LS2) )

assume x in Carrier (LS1 + LS2) ; :: thesis: x in (Carrier LS1) \/ (Carrier LS2)

then consider u being Element of S such that

A18: x = u and

A19: (LS1 + LS2) . u <> 0 ;

(LS1 + LS2) . u = (LS1 . u) + (LS2 . u) by RLVECT_2:def 10;

then ( LS1 . u <> 0 or LS2 . u <> 0 ) by A19;

then ( x in Carrier LS1 or x in Carrier LS2 ) by A18;

hence x in (Carrier LS1) \/ (Carrier LS2) by XBOOLE_0:def 3; :: thesis: verum

end;assume x in Carrier (LS1 + LS2) ; :: thesis: x in (Carrier LS1) \/ (Carrier LS2)

then consider u being Element of S such that

A18: x = u and

A19: (LS1 + LS2) . u <> 0 ;

(LS1 + LS2) . u = (LS1 . u) + (LS2 . u) by RLVECT_2:def 10;

then ( LS1 . u <> 0 or LS2 . u <> 0 ) by A19;

then ( x in Carrier LS1 or x in Carrier LS2 ) by A18;

hence x in (Carrier LS1) \/ (Carrier LS2) by XBOOLE_0:def 3; :: thesis: verum

hence sum (LS1 + LS2) = Sum (L1p + L2p) by A9, A14, A17, Th30

.= (sum LS1) + (sum LS2) by A13, A16, RVSUM_1:89 ;

:: thesis: verum