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)
proof
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;
(p112 ^ p12) ^ p211 is one-to-one by A5, A6, A7, A8, A15, FINSEQ_3:91;
hence sum (LS1 + LS2) = Sum (L1p + L2p) by A9, A14, A17, Th30
.= (sum LS1) + (sum LS2) by A13, A16, RVSUM_1:89 ;
:: thesis: verum