let R be Ring; :: thesis: for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W
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 LeftMod of R; :: thesis: for l being Linear_Combination of V
for T being linear-transformation of V,W
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 T being linear-transformation of V,W
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 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
v in the carrier of V ;
then A3: v in dom l by FUNCT_2:def 1;
A4: dom T = the carrier of V by FUNCT_2:def 1;
for x being object holds
( x in (T " {(T . v)}) /\ (Carrier l) iff x in {v} )

proof

let x be object ; :: thesis: ( x in (T " {(T . v)}) /\ (Carrier l) iff x in {v} )

hereby :: thesis: ( x in {v} implies x in (T " {(T . v)}) /\ (Carrier l) )

assume x in (T " {(T . v)}) /\ (Carrier l) ; :: thesis: x in {v}
then A5: ( x in T " {(T . v)} & x in Carrier l ) by XBOOLE_0:def 4;
then A6: ( x in the carrier of V & T . x in {(T . v)} ) by FUNCT_2:38;
A7: (T | (Carrier l)) . x = T . x by A5, FUNCT_1:49
.= T . v by A6, TARSKI:def 1
.= (T | (Carrier l)) . v by A2, FUNCT_1:49 ;
A8: x in dom (T | (Carrier l)) by A4, A5, RELAT_1:57;
v in dom (T | (Carrier l)) by A2, A4, RELAT_1:57;
then x = v by A1, A7, A8, FUNCT_1:def 4;
hence x in {v} by TARSKI:def 1; :: thesis: verum

end;

assume x in {v} ; :: thesis: x in (T " {(T . v)}) /\ (Carrier l)
then A9: x = v by TARSKI:def 1;
( x in the carrier of V & T . x in {(T . v)} ) by A9, TARSKI:def 1;
then x in T " {(T . v)} by FUNCT_2:38;
hence x in (T " {(T . v)}) /\ (Carrier l) by A2, A9, XBOOLE_0:def 4; :: thesis: verum

end;

then (T " {(T . v)}) /\ (Carrier l) = {v} by TARSKI:2;
then canFS ((T " {(T . v)}) /\ (Carrier l)) = <*v*> by FINSEQ_1:94;
then lCFST (l,T,(T . v)) = <*(l . v)*> by A3, FINSEQ_2:34;
then Sum (lCFST (l,T,(T . v))) = l . v by RLVECT_1:44;
hence (T @* l) . (T . v) = l . v by LDef5; :: thesis: verum