let r be Real; :: thesis: for V being RealLinearSpace

for L being Linear_Combination of V

for F being FinSequence of V holds (r * L) * F = r * (L * F)

let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V

for F being FinSequence of V holds (r * L) * F = r * (L * F)

let L be Linear_Combination of V; :: thesis: for F being FinSequence of V holds (r * L) * F = r * (L * F)

let p be FinSequence of V; :: thesis: (r * L) * p = r * (L * p)

A1: len ((r * L) * p) = len p by FINSEQ_2:33;

A2: len (L * p) = len p by FINSEQ_2:33;

then reconsider rLp = (r * L) * p, Lp = L * p as Element of (len p) -tuples_on REAL by A1, FINSEQ_2:92;

hence (r * L) * p = r * (L * p) by A1, A3; :: thesis: verum

for L being Linear_Combination of V

for F being FinSequence of V holds (r * L) * F = r * (L * F)

let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V

for F being FinSequence of V holds (r * L) * F = r * (L * F)

let L be Linear_Combination of V; :: thesis: for F being FinSequence of V holds (r * L) * F = r * (L * F)

let p be FinSequence of V; :: thesis: (r * L) * p = r * (L * p)

A1: len ((r * L) * p) = len p by FINSEQ_2:33;

A2: len (L * p) = len p by FINSEQ_2:33;

then reconsider rLp = (r * L) * p, Lp = L * p as Element of (len p) -tuples_on REAL by A1, FINSEQ_2:92;

A3: now :: thesis: for k being Nat st 1 <= k & k <= len p holds

rLp . k = (r * Lp) . k

len (r * Lp) = len p
by CARD_1:def 7;rLp . k = (r * Lp) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len p implies rLp . k = (r * Lp) . k )

assume A4: ( 1 <= k & k <= len p ) ; :: thesis: rLp . k = (r * Lp) . k

then k in dom Lp by A2, FINSEQ_3:25;

then A5: ( Lp . k = L . (p . k) & p . k in dom L ) by FUNCT_1:11, FUNCT_1:12;

k in dom rLp by A1, A4, FINSEQ_3:25;

then A6: rLp . k = (r * L) . (p . k) by FUNCT_1:12;

( (r * Lp) . k = r * (Lp . k) & dom L = the carrier of V ) by FUNCT_2:def 1, RVSUM_1:44;

hence rLp . k = (r * Lp) . k by A5, A6, RLVECT_2:def 11; :: thesis: verum

end;assume A4: ( 1 <= k & k <= len p ) ; :: thesis: rLp . k = (r * Lp) . k

then k in dom Lp by A2, FINSEQ_3:25;

then A5: ( Lp . k = L . (p . k) & p . k in dom L ) by FUNCT_1:11, FUNCT_1:12;

k in dom rLp by A1, A4, FINSEQ_3:25;

then A6: rLp . k = (r * L) . (p . k) by FUNCT_1:12;

( (r * Lp) . k = r * (Lp . k) & dom L = the carrier of V ) by FUNCT_2:def 1, RVSUM_1:44;

hence rLp . k = (r * Lp) . k by A5, A6, RLVECT_2:def 11; :: thesis: verum

hence (r * L) * p = r * (L * p) by A1, A3; :: thesis: verum