let F be Field; :: thesis: for U, V being VectSp of F
for B being non empty finite Subset of U
for f being Function of B,V
for l1, l2 being Linear_Combination of B
for a being Element of F st l2 = a * l1 holds
f (#) l2 = a * (f (#) l1)
let U, V be VectSp of F; :: thesis: for B being non empty finite Subset of U
for f being Function of B,V
for l1, l2 being Linear_Combination of B
for a being Element of F st l2 = a * l1 holds
f (#) l2 = a * (f (#) l1)
let B be non empty finite Subset of U; :: thesis: for f being Function of B,V
for l1, l2 being Linear_Combination of B
for a being Element of F st l2 = a * l1 holds
f (#) l2 = a * (f (#) l1)
let f be Function of B,V; :: thesis: for l1, l2 being Linear_Combination of B
for a being Element of F st l2 = a * l1 holds
f (#) l2 = a * (f (#) l1)
let l1, l2 be Linear_Combination of B; :: thesis: for a being Element of F st l2 = a * l1 holds
f (#) l2 = a * (f (#) l1)
let a be Element of F; :: thesis: ( l2 = a * l1 implies f (#) l2 = a * (f (#) l1) )
assume AS: l2 = a * l1 ; :: thesis: f (#) l2 = a * (f (#) l1)
U: ( dom l1 = the carrier of U & dom l2 = the carrier of U ) by FUNCT_2:def 1;

now :: thesis: for v being Element of V holds (f (#) l2) . v = (a * (f (#) l1)) . v

let v be Element of V; :: thesis: (f (#) l2) . b₁ = (a * (f (#) l1)) . b₁

per cases ( v in rng f or not v in rng f ) ;

suppose v in rng f ; :: thesis: (f (#) l2) . b₁ = (a * (f (#) l1)) . b₁

then consider x being object such that
C1: ( x in dom f & f . x = v ) by FUNCT_1:def 3;
reconsider u = x as Element of B by C1;
set T1 = Expand (f,l1,v);
set T2 = Expand (f,l2,v);
KP: len (a * (Expand (f,l1,v))) = len (Expand (f,l1,v)) by MATRIXR1:16;
V: len (canFS (f " {v})) = card (f " {v}) by FINSEQ_1:93;
( rng (canFS (f " {v})) = f " {v} & f " {v} c= B & B c= the carrier of U ) by FUNCT_2:def 3;
then W: ( rng (canFS (f " {v})) c= dom l1 & rng (canFS (f " {v})) c= dom l2 ) by U;
then K: len (Expand (f,l1,v)) = card (f " {v}) by V, FINSEQ_2:29
.= len (Expand (f,l2,v)) by V, W, FINSEQ_2:29 ;

now :: thesis: for i being Nat st 1 <= i & i <= len (Expand (f,l2,v)) holds
(Expand (f,l2,v)) . i = (a * (Expand (f,l1,v))) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len (Expand (f,l2,v)) implies (Expand (f,l2,v)) . i = (a * (Expand (f,l1,v))) . i )
assume ( 1 <= i & i <= len (Expand (f,l2,v)) ) ; :: thesis: (Expand (f,l2,v)) . i = (a * (Expand (f,l1,v))) . i
then E0: ( i in dom (Expand (f,l2,v)) & i in dom (Expand (f,l1,v)) & i in dom (a * (Expand (f,l1,v))) ) by FINSEQ_3:25, K, KP;
then E1: i in dom (canFS (f " {v})) by FUNCT_1:11;
then E2: (canFS (f " {v})) . i in rng (canFS (f " {v})) by FUNCT_1:3;
( rng (canFS (f " {v})) = f " {v} & f " {v} c= B & B c= the carrier of U ) by FUNCT_2:def 3;
then reconsider w = (canFS (f " {v})) . i as Element of U by E2;
E3: (Expand (f,l1,v)) /. i = (l1 * (canFS (f " {v}))) . i by E0, PARTFUN1:def 6
.= l1 . w by E1, FUNCT_1:13 ;
E4: (Expand (f,l1,v)) /. i = (Expand (f,l1,v)) . i by E0, PARTFUN1:def 6;
thus (Expand (f,l2,v)) . i = l2 . ((canFS (f " {v})) . i) by E1, FUNCT_1:13
.= a * ((Expand (f,l1,v)) /. i) by E3, AS, VECTSP_6:def 9
.= (a * (Expand (f,l1,v))) . i by E4, E0, FVSUM_1:50 ; :: thesis: verum

end;

then EE: Expand (f,l2,v) = a * (Expand (f,l1,v)) by K, MATRIXR1:16;
reconsider fl1 = f (#) l1 as Linear_Combination of V ;
thus (f (#) l2) . v = Sum (Expand (f,l2,v)) by defK
.= a * (Sum (Expand (f,l1,v))) by EE, BINOM:4
.= a * (fl1 . v) by defK
.= (a * (f (#) l1)) . v by VECTSP_6:def 9 ; :: thesis: verum

end;

suppose C0: not v in rng f ; :: thesis: (f (#) l2) . b₁ = (a * (f (#) l1)) . b₁

hence (f (#) l2) . v = a * (0. F) by lemadd2b
.= a * ((f (#) l1) . v) by C0, lemadd2b
.= (a * (f (#) l1)) . v by VECTSP_6:def 9 ;
:: thesis: verum

end;

end;

end;

hence f (#) l2 = a * (f (#) l1) by VECTSP_6:def 7; :: thesis: verum