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, l3 being Linear_Combination of B st l3 = l1 + l2 holds
f (#) l3 = (f (#) l1) + (f (#) l2)
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, l3 being Linear_Combination of B st l3 = l1 + l2 holds
f (#) l3 = (f (#) l1) + (f (#) l2)
let B be non empty finite Subset of U; :: thesis: for f being Function of B,V
for l1, l2, l3 being Linear_Combination of B st l3 = l1 + l2 holds
f (#) l3 = (f (#) l1) + (f (#) l2)
let f be Function of B,V; :: thesis: for l1, l2, l3 being Linear_Combination of B st l3 = l1 + l2 holds
f (#) l3 = (f (#) l1) + (f (#) l2)
let l1, l2, l3 be Linear_Combination of B; :: thesis: ( l3 = l1 + l2 implies f (#) l3 = (f (#) l1) + (f (#) l2) )
assume AS: l3 = l1 + l2 ; :: thesis: f (#) l3 = (f (#) l1) + (f (#) l2)
U: ( dom l1 = the carrier of U & dom l2 = the carrier of U & dom l3 = the carrier of U ) by FUNCT_2:def 1;

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

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

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

suppose v in rng f ; :: thesis: (f (#) l3) . b₁ = ((f (#) l1) + (f (#) l2)) . 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 T3 = Expand (f,l3,v);
set T1 = Expand (f,l1,v);
set T2 = Expand (f,l2,v);
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 & rng (canFS (f " {v})) c= dom l3 ) 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 ;
KP: len (Expand (f,l1,v)) = card (f " {v}) by W, V, FINSEQ_2:29
.= len (Expand (f,l3,v)) by V, W, FINSEQ_2:29 ;

E: now :: thesis: for i being Nat st i in dom (Expand (f,l1,v)) holds
(Expand (f,l3,v)) . i = ((Expand (f,l1,v)) /. i) + ((Expand (f,l2,v)) /. i)

let i be Nat; :: thesis: ( i in dom (Expand (f,l1,v)) implies (Expand (f,l3,v)) . i = ((Expand (f,l1,v)) /. i) + ((Expand (f,l2,v)) /. i) )
assume E0: i in dom (Expand (f,l1,v)) ; :: thesis: (Expand (f,l3,v)) . i = ((Expand (f,l1,v)) /. i) + ((Expand (f,l2,v)) /. i)
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 ;
w in dom l2 by U;
then i in dom (l2 * (canFS (f " {v}))) by E1, FUNCT_1:11;
then E4: (Expand (f,l2,v)) /. i = (l2 * (canFS (f " {v}))) . i by PARTFUN1:def 6
.= l2 . w by E1, FUNCT_1:13 ;
thus (Expand (f,l3,v)) . i = l3 . ((canFS (f " {v})) . i) by E1, FUNCT_1:13
.= ((Expand (f,l1,v)) /. i) + ((Expand (f,l2,v)) /. i) by E3, E4, AS, VECTSP_6:22 ; :: thesis: verum

end;

C: Sum (Expand (f,l3,v)) = (Sum (Expand (f,l1,v))) + (Sum (Expand (f,l2,v))) by E, K, KP, RLVECT_2:2;
thus (f (#) l3) . v = Sum (Expand (f,l3,v)) by defK
.= (Sum (Expand (f,l1,v))) + ((f (#) l2) . v) by C, defK
.= ((f (#) l1) . v) + ((f (#) l2) . v) by defK
.= ((f (#) l1) + (f (#) l2)) . v by VECTSP_6:22 ; :: thesis: verum

end;

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

then (f (#) l1) . v = 0. F by lemadd2b;
hence ((f (#) l1) + (f (#) l2)) . v = (0. F) + ((f (#) l2) . v) by VECTSP_6:22
.= 0. F by C0, lemadd2b
.= (f (#) l3) . v by C0, lemadd2b ;
:: thesis: verum

end;

end;

end;

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