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;

hence (LS1 + LS2) * p = (LS1 * p) + (LS2 * p) by A3, A4; :: thesis: verum

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

len (L1p + L2p) = len p
by CARD_1:def 7;((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;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

hence (LS1 + LS2) * p = (LS1 * p) + (LS2 * p) by A3, A4; :: thesis: verum