let F be Field; :: thesis: for U, V being finite-dimensional VectSp of F
for B being Basis of U
for f being Function of B,V
for T being linear-transformation of U,V holds
( T = canLinTrans f iff for u being Element of U st u in B holds
T . u = f . u )
let U, V be finite-dimensional VectSp of F; :: thesis: for B being Basis of U
for f being Function of B,V
for T being linear-transformation of U,V holds
( T = canLinTrans f iff for u being Element of U st u in B holds
T . u = f . u )
let B be Basis of U; :: thesis: for f being Function of B,V
for T being linear-transformation of U,V holds
( T = canLinTrans f iff for u being Element of U st u in B holds
T . u = f . u )
let f be Function of B,V; :: thesis: for T being linear-transformation of U,V holds
( T = canLinTrans f iff for u being Element of U st u in B holds
T . u = f . u )
let T be linear-transformation of U,V; :: thesis: ( T = canLinTrans f iff for u being Element of U st u in B holds
T . u = f . u )
H: dom f = B by FUNCT_2:def 1;

A: now :: thesis: ( T = canLinTrans f implies for u being Element of U st u in B holds
T . u = f . u )

assume T = canLinTrans f ; :: thesis: for u being Element of U st u in B holds
T . u = f . u
then T | B = f by defcl;
hence for u being Element of U st u in B holds
T . u = f . u by FUNCT_1:49; :: thesis: verum

end;

now :: thesis: ( ( for u being Element of U st u in B holds
T . u = f . u ) implies T = canLinTrans f )

assume C: for u being Element of U st u in B holds
T . u = f . u ; :: thesis: T = canLinTrans f

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

let x be object ; :: thesis: ( x in dom f implies f . x = T . x )
assume x in dom f ; :: thesis: f . x = T . x
then x in B ;
hence f . x = T . x by C; :: thesis: verum

end;

( dom T = the carrier of U & B c= the carrier of U ) by FUNCT_2:def 1;
then dom f = (dom T) /\ B by H, XBOOLE_1:28;
then T | B = f by D, FUNCT_1:46;
hence T = canLinTrans f by defcl; :: thesis: verum

end;

hence ( T = canLinTrans f iff for u being Element of U st u in B holds
T . u = f . u ) by A; :: thesis: verum