let F be Field; :: thesis: for U being non trivial finite-dimensional VectSp of F
for V being VectSp of F
for B being Basis of U
for f being Function of B,V
for l being Linear_Combination of B holds (canLinTrans f) . (Sum l) = Sum (f (#) l)
let U be non trivial finite-dimensional VectSp of F; :: thesis: for V being VectSp of F
for B being Basis of U
for f being Function of B,V
for l being Linear_Combination of B holds (canLinTrans f) . (Sum l) = Sum (f (#) l)
let V be VectSp of F; :: thesis: for B being Basis of U
for f being Function of B,V
for l being Linear_Combination of B holds (canLinTrans f) . (Sum l) = Sum (f (#) l)
let B be Basis of U; :: thesis: for f being Function of B,V
for l being Linear_Combination of B holds (canLinTrans f) . (Sum l) = Sum (f (#) l)
let f be Function of B,V; :: thesis: for l being Linear_Combination of B holds (canLinTrans f) . (Sum l) = Sum (f (#) l)
let l be Linear_Combination of B; :: thesis: (canLinTrans f) . (Sum l) = Sum (f (#) l)
set B1 = B;
B: Lin B = ModuleStr(# the carrier of U, the addF of U, the ZeroF of U, the lmult of U #) by VECTSP_7:def 3;
defpred S₁[ object , object ] means for l being Linear_Combination of B st $1 = Sum l holds
$2 = Sum (f (#) l);

AA: now :: thesis: for x being object st x in the carrier of U holds
ex y being object st
( y in the carrier of V & S₁[x,y] )

let x be object ; :: thesis: ( x in the carrier of U implies ex y being object st
( y in the carrier of V & S₁[x,y] ) )
assume x in the carrier of U ; :: thesis: ex y being object st
( y in the carrier of V & S₁[x,y] )
then reconsider u = x as Element of U ;
u in the carrier of (Lin B) by B;
then u in { (Sum l) where l is Linear_Combination of B : verum } by VECTSP_7:def 2;
then consider l being Linear_Combination of B such that
C1: u = Sum l ;
thus ex y being object st
( y in the carrier of V & S₁[x,y] ) :: thesis: verum

proof

take Sum (f (#) l) ; :: thesis: ( Sum (f (#) l) in the carrier of V & S₁[x, Sum (f (#) l)] )
thus ( Sum (f (#) l) in the carrier of V & S₁[x, Sum (f (#) l)] ) by C1, FIELD_7:6; :: thesis: verum

end;

end;

consider T being Function of the carrier of U, the carrier of V such that
A: for u being object st u in the carrier of U holds
S₁[u,T . u] from FUNCT_2:sch 1(AA);

C: now :: thesis: for u1, u2 being Element of U holds (T . u1) + (T . u2) = T . (u1 + u2)

let u1, u2 be Element of U; :: thesis: (T . u1) + (T . u2) = T . (u1 + u2)
u1 in the carrier of (Lin B) by B;
then u1 in { (Sum l) where l is Linear_Combination of B : verum } by VECTSP_7:def 2;
then consider l1 being Linear_Combination of B such that
C1: u1 = Sum l1 ;
u2 in the carrier of (Lin B) by B;
then u2 in { (Sum l) where l is Linear_Combination of B : verum } by VECTSP_7:def 2;
then consider l2 being Linear_Combination of B such that
C2: u2 = Sum l2 ;
reconsider l3 = l1 + l2 as Linear_Combination of B by VECTSP_6:24;
thus (T . u1) + (T . u2) = (Sum (f (#) l1)) + (T . (Sum l2)) by A, C1, C2
.= (Sum (f (#) l1)) + (Sum (f (#) l2)) by A
.= Sum (f (#) l3) by lemadd
.= T . (Sum (l1 + l2)) by A
.= T . (u1 + u2) by C1, C2, VECTSP_6:44 ; :: thesis: verum

end;

now :: thesis: for a being Element of F
for u being Element of U holds a * (T . u) = T . (a * u)

let a be Element of F; :: thesis: for u being Element of U holds a * (T . u) = T . (a * u)
let u be Element of U; :: thesis: a * (T . u) = T . (a * u)
u in the carrier of (Lin B) by B;
then u in { (Sum l) where l is Linear_Combination of B : verum } by VECTSP_7:def 2;
then consider l being Linear_Combination of B such that
C1: u = Sum l ;
reconsider al = a * l as Linear_Combination of B by VECTSP_6:31;
thus a * (T . u) = a * (Sum (f (#) l)) by A, C1
.= Sum (f (#) al) by lemmult
.= T . (Sum al) by A
.= T . (a * u) by C1, VECTSP_6:45 ; :: thesis: verum

end;

then reconsider T = T as linear-transformation of U,V by C, VECTSP_1:def 20, MOD_2:def 2;
B c= the carrier of U ;
then B c= dom T by FUNCT_2:def 1;
then E: (dom T) /\ B = B by XBOOLE_1:28
.= dom f by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom f holds
T . x = f . x

let x be object ; :: thesis: ( x in dom f implies T . x = f . x )
assume x in dom f ; :: thesis: T . x = f . x
then reconsider w = x as Element of B ;
w in the carrier of (Lin B) by B;
then w in { (Sum l) where l is Linear_Combination of B : verum } by VECTSP_7:def 2;
then consider l being Linear_Combination of B such that
C1: w = Sum l ;
thus T . x = Sum (f (#) l) by C1, A
.= f . x by C1, lembas ; :: thesis: verum

end;

then T | B = f by E, FUNCT_1:46
.= (canLinTrans f) | B by defcl ;
then T = canLinTrans f by canLinuni;
hence (canLinTrans f) . (Sum l) = Sum (f (#) l) by A; :: thesis: verum