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} )

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

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

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

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;hereby :: thesis: ( x in {v} implies x in (T " {(T . v)}) /\ (Carrier l) )

assume
x in {v}
; :: thesis: 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;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

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

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