let F be Field; :: thesis: for V, W being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds
(T @ l) . (T . v) = l . v
let V, W be VectSp of F; :: thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V
for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds
(T @ l) . (T . v) = l . v
let T be linear-transformation of V,W; :: thesis: for l being Linear_Combination of V
for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds
(T @ l) . (T . v) = l . v
let l be Linear_Combination of V; :: thesis: for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds
(T @ l) . (T . v) = l . v
let v be Element of V; :: thesis: ( T | (Carrier l) is one-to-one & v in Carrier l implies (T @ l) . (T . v) = l . v )
assume that
A1: T | (Carrier l) is one-to-one and
A2: v in Carrier l ; :: thesis: (T @ l) . (T . v) = l . v
consider X being Subset of V such that
A3: X misses Carrier l and
A4: T " {(T . v)} = {v} \/ X by A1, A2, Th34;

per cases ( X = {} or X <> {} ) ;

suppose A5: X = {} ; :: thesis: (T @ l) . (T . v) = l . v

A6: dom l = [#] V by FUNCT_2:92;
l .: {v} = Im (l,v)
.= {(l . v)} by A6, FUNCT_1:59 ;
then Sum (l .: (T " {(T . v)})) = l . v by A4, A5, RLVECT_2:9;
hence (T @ l) . (T . v) = l . v by Def5; :: thesis: verum

end;

suppose A7: X <> {} ; :: thesis: (T @ l) . (T . v) = l . v

A8: l .: X c= {(0. F)}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in l .: X or y in {(0. F)} )
assume y in l .: X ; :: thesis: y in {(0. F)}
then consider x being object such that
A9: x in dom l and
A10: x in X and
A11: y = l . x by FUNCT_1:def 6;
A12: not x in Carrier l by A3, A10, XBOOLE_0:def 4;
reconsider x = x as Element of V by A9;
l . x = 0. F by A12;
hence y in {(0. F)} by A11, TARSKI:def 1; :: thesis: verum

end;

A13: l .: X misses l .: {v}

proof

assume l .: X meets l .: {v} ; :: thesis: contradiction
then consider x being object such that
A14: x in l .: X and
A15: x in l .: {v} by XBOOLE_0:3;
A16: dom l = [#] V by FUNCT_2:92;
l .: {v} = Im (l,v)
.= {(l . v)} by A16, FUNCT_1:59 ;
then A17: x = l . v by A15, TARSKI:def 1;
x = 0. F by A8, A14, TARSKI:def 1;
hence contradiction by A2, A17, VECTSP_6:2; :: thesis: verum

end;

A18: dom l = [#] V by FUNCT_2:92;
{(0. F)} c= l .: X

proof

consider y being object such that
A19: y in X by A7, XBOOLE_0:def 1;
A20: not y in Carrier l by A3, A19, XBOOLE_0:def 4;
reconsider y = y as Element of V by A19;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. F)} or x in l .: X )
assume x in {(0. F)} ; :: thesis: x in l .: X
then x = 0. F by TARSKI:def 1;
then l . y = x by A20;
hence x in l .: X by A18, A19, FUNCT_1:def 6; :: thesis: verum

end;

then A21: l .: X = {(0. F)} by A8;
A22: l .: {v} = Im (l,v)
.= {(l . v)} by A18, FUNCT_1:59 ;
l .: (T " {(T . v)}) = (l .: {v}) \/ (l .: X) by A4, RELAT_1:120;
then Sum (l .: (T " {(T . v)})) = (Sum (l .: {v})) + (Sum (l .: X)) by A13, RLVECT_2:12
.= (l . v) + (Sum {(0. F)}) by A22, A21, RLVECT_2:9
.= (l . v) + (0. F) by RLVECT_2:9
.= l . v by RLVECT_1:4 ;
hence (T @ l) . (T . v) = l . v by Def5; :: thesis: verum

end;

end;