let S be non empty addLoopStr ; :: thesis: for LS1, LS2 being Linear_Combination of S
for F being FinSequence of S holds (LS1 + LS2) * F = (LS1 * F) + (LS2 * F)
let LS1, LS2 be Linear_Combination of S; :: thesis: for F being FinSequence of S holds (LS1 + LS2) * F = (LS1 * F) + (LS2 * F)
let p be FinSequence of S; :: thesis: (LS1 + LS2) * p = (LS1 * p) + (LS2 * p)
A1: len (LS1 * p) = len p by FINSEQ_2:33;
A2: len (LS2 * p) = len p by FINSEQ_2:33;
then reconsider L1p = LS1 * p, L2p = LS2 * p as Element of (len p) -tuples_on REAL by A1, FINSEQ_2:92;
A3: len ((LS1 + LS2) * p) = len p by FINSEQ_2:33;

A4: now :: thesis: for k being Nat st 1 <= k & k <= len p holds
((LS1 + LS2) * p) . k = (L1p + L2p) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len p implies ((LS1 + LS2) * p) . k = (L1p + L2p) . k )
assume A5: ( 1 <= k & k <= len p ) ; :: thesis: ((LS1 + LS2) * p) . k = (L1p + L2p) . k
then k in dom ((LS1 + LS2) * p) by A3, FINSEQ_3:25;
then A6: ((LS1 + LS2) * p) . k = (LS1 + LS2) . (p . k) by FUNCT_1:12;
k in dom L1p by A1, A5, FINSEQ_3:25;
then A7: ( p . k in dom LS1 & L1p . k = LS1 . (p . k) ) by FUNCT_1:11, FUNCT_1:12;
k in dom L2p by A2, A5, FINSEQ_3:25;
then A8: L2p . k = LS2 . (p . k) by FUNCT_1:12;
dom LS1 = the carrier of S by FUNCT_2:def 1;
hence ((LS1 + LS2) * p) . k = (L1p . k) + (L2p . k) by A6, A8, A7, RLVECT_2:def 10
.= (L1p + L2p) . k by RVSUM_1:11 ;
:: thesis: verum

end;

len (L1p + L2p) = len p by CARD_1:def 7;
hence (LS1 + LS2) * p = (LS1 * p) + (LS2 * p) by A3, A4; :: thesis: verum