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;
A3: now :: thesis: for k being Nat st 1 <= k & k <= len p holds
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;
len (r * Lp) = len p by CARD_1:def 7;
hence (r * L) * p = r * (L * p) by A1, A3; :: thesis: verum