let R be Ring; :: thesis: for V, W being LeftMod of R

for X being Subset of V

for T being linear-transformation of V,W

for X being Subset of V

for l being Linear_Combination of T .: X

for v being Element of V st v in X & T | X is one-to-one holds

(T # l) . v = l . (T . v)

let V, W be LeftMod of R; :: thesis: for X being Subset of V

for T being linear-transformation of V,W

for X being Subset of V

for l being Linear_Combination of T .: X

for v being Element of V st v in X & T | X is one-to-one holds

(T # l) . v = l . (T . v)

let X be Subset of V; :: thesis: for T being linear-transformation of V,W

for X being Subset of V

for l being Linear_Combination of T .: X

for v being Element of V st v in X & T | X is one-to-one holds

(T # l) . v = l . (T . v)

let T be linear-transformation of V,W; :: thesis: for X being Subset of V

for l being Linear_Combination of T .: X

for v being Element of V st v in X & T | X is one-to-one holds

(T # l) . v = l . (T . v)

let X be Subset of V; :: thesis: for l being Linear_Combination of T .: X

for v being Element of V st v in X & T | X is one-to-one holds

(T # l) . v = l . (T . v)

let l be Linear_Combination of T .: X; :: thesis: for v being Element of V st v in X & T | X is one-to-one holds

(T # l) . v = l . (T . v)

let v be Element of V; :: thesis: ( v in X & T | X is one-to-one implies (T # l) . v = l . (T . v) )

assume ( v in X & T | X is one-to-one ) ; :: thesis: (T # l) . v = l . (T . v)

then ( not v in dom ((X `) --> (0. R)) & T # l = (l * T) +* ((X `) --> (0. R)) ) by Def6, XBOOLE_0:def 5;

then A1: (T # l) . v = (l * T) . v by FUNCT_4:11;

dom T = [#] V by RANKNULL:7;

hence (T # l) . v = l . (T . v) by A1, FUNCT_1:13; :: thesis: verum

for X being Subset of V

for T being linear-transformation of V,W

for X being Subset of V

for l being Linear_Combination of T .: X

for v being Element of V st v in X & T | X is one-to-one holds

(T # l) . v = l . (T . v)

let V, W be LeftMod of R; :: thesis: for X being Subset of V

for T being linear-transformation of V,W

for X being Subset of V

for l being Linear_Combination of T .: X

for v being Element of V st v in X & T | X is one-to-one holds

(T # l) . v = l . (T . v)

let X be Subset of V; :: thesis: for T being linear-transformation of V,W

for X being Subset of V

for l being Linear_Combination of T .: X

for v being Element of V st v in X & T | X is one-to-one holds

(T # l) . v = l . (T . v)

let T be linear-transformation of V,W; :: thesis: for X being Subset of V

for l being Linear_Combination of T .: X

for v being Element of V st v in X & T | X is one-to-one holds

(T # l) . v = l . (T . v)

let X be Subset of V; :: thesis: for l being Linear_Combination of T .: X

for v being Element of V st v in X & T | X is one-to-one holds

(T # l) . v = l . (T . v)

let l be Linear_Combination of T .: X; :: thesis: for v being Element of V st v in X & T | X is one-to-one holds

(T # l) . v = l . (T . v)

let v be Element of V; :: thesis: ( v in X & T | X is one-to-one implies (T # l) . v = l . (T . v) )

assume ( v in X & T | X is one-to-one ) ; :: thesis: (T # l) . v = l . (T . v)

then ( not v in dom ((X `) --> (0. R)) & T # l = (l * T) +* ((X `) --> (0. R)) ) by Def6, XBOOLE_0:def 5;

then A1: (T # l) . v = (l * T) . v by FUNCT_4:11;

dom T = [#] V by RANKNULL:7;

hence (T # l) . v = l . (T . v) by A1, FUNCT_1:13; :: thesis: verum