let F be Field; :: thesis: for X, Y being VectSp of F
for l being Linear_Combination of X
for T being linear-transformation of X,Y st T is one-to-one holds
T @ l = T @* l
let X, Y be VectSp of F; :: thesis: for l being Linear_Combination of X
for T being linear-transformation of X,Y st T is one-to-one holds
T @ l = T @* l
let l be Linear_Combination of X; :: thesis: for T being linear-transformation of X,Y st T is one-to-one holds
T @ l = T @* l
let T be linear-transformation of X,Y; :: thesis: ( T is one-to-one implies T @ l = T @* l )
assume AS: T is one-to-one ; :: thesis: T @ l = T @* l
A1: Carrier (T @ l) c= T .: (Carrier l) by RANKNULL:30;
for y being Element of Y holds (T @ l) . y = Sum (lCFST (l,T,y))

proof

let y be Element of Y; :: thesis: (T @ l) . y = Sum (lCFST (l,T,y))
rng (lCFST (l,T,y)) c= the carrier of F ;
then reconsider Z = lCFST (l,T,y) as FinSequence of F by FINSEQ_1:def 4;
C0: (T @ l) . y = Sum (l .: (T " {y})) by RANKNULL:def 5;

per cases ( T " {y} = {} or T " {y} <> {} ) ;

suppose C1: T " {y} = {} ; :: thesis: (T @ l) . y = Sum (lCFST (l,T,y))

then lCFST (l,T,y) = <*> the carrier of F ;
then C2: Sum (lCFST (l,T,y)) = 0. F by RLVECT_1:43;
l .: (T " {y}) = {} F by C1;
hence (T @ l) . y = Sum (lCFST (l,T,y)) by C0, C2, RLVECT_2:8; :: thesis: verum

end;

suppose T " {y} <> {} ; :: thesis: (T @ l) . y = Sum (lCFST (l,T,y))

then consider x being object such that
X1: x in T " {y} by XBOOLE_0:def 1;
X2: ( x in dom T & T . x in {y} ) by X1, FUNCT_1:def 7;
reconsider x = x as Element of X by X1;
C2: T . x = y by X2, TARSKI:def 1;
y in rng T by X2, C2, FUNCT_1:def 3;
then C3: ex x0 being object st T " {y} = {x0} by AS, FUNCT_1:74;
then C31: T " {y} = {x} by X1, TARSKI:def 1;
C81: dom l = the carrier of X by FUNCT_2:def 1;
C9: l .: (T " {y}) = Im (l,x) by C3, X1, TARSKI:def 1
.= {(l . x)} by C81, FUNCT_1:59 ;

per cases ( x in Carrier l or not x in Carrier l ) ;

suppose C61: x in Carrier l ; :: thesis: (T @ l) . y = Sum (lCFST (l,T,y))

then C6: (T " {y}) /\ (Carrier l) = {x} by C31, XBOOLE_1:28, ZFMISC_1:31;
dom l = the carrier of X by FUNCT_2:def 1;
then rng (canFS ((T " {y}) /\ (Carrier l))) c= dom l by XBOOLE_1:1;
then C81: dom Z = dom (canFS ((T " {y}) /\ (Carrier l))) by RELAT_1:27
.= dom (canFS {x}) by C31, C61, XBOOLE_1:28, ZFMISC_1:31
.= dom <*x*> by FINSEQ_1:94
.= Seg 1 by FINSEQ_1:38 ;
then C82: len Z = 1 by FINSEQ_1:def 3;
1 in dom Z by C81;
then Z . 1 = l . ((canFS {x}) . 1) by C6, FUNCT_1:12
.= l . (<*x*> . 1) by FINSEQ_1:94
.= l . x ;
then C83: Z = <*(l . x)*> by FINSEQ_1:40, C82;
then C8: Z = canFS {(l . x)} by FINSEQ_1:94;
rng Z = l .: (T " {y}) by C9, C83, FINSEQ_1:38;
hence (T @ l) . y = Sum (lCFST (l,T,y)) by C0, C8, RLVECT_2:def 2; :: thesis: verum

end;

suppose C5: not x in Carrier l ; :: thesis: (T @ l) . y = Sum (lCFST (l,T,y))

(T " {y}) /\ (Carrier l) = {}

proof

assume (T " {y}) /\ (Carrier l) <> {} ; :: thesis: contradiction
then consider x0 being object such that
C60: x0 in (T " {y}) /\ (Carrier l) by XBOOLE_0:def 1;
( x0 in T " {y} & x0 in Carrier l ) by C60, XBOOLE_0:def 4;
hence contradiction by C5, C31, TARSKI:def 1; :: thesis: verum

end;

then Z = <*> the carrier of F ;
then C8: Sum (lCFST (l,T,y)) = 0. F by RLVECT_1:43;
l .: (T " {y}) = {(0. F)} by C5, C9;
hence (T @ l) . y = Sum (lCFST (l,T,y)) by C0, C8, RLVECT_2:9; :: thesis: verum

end;

end;

end;

end;

end;

hence T @ l = T @* l by A1, ZMODUL05:def 8; :: thesis: verum