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

for l being Linear_Combination of V

for A being Subset of V

for v being Element of V st v in A holds

(l ! A) . v = l . v

let V be LeftMod of R; :: thesis: for l being Linear_Combination of V

for A being Subset of V

for v being Element of V st v in A holds

(l ! A) . v = l . v

let l be Linear_Combination of V; :: thesis: for A being Subset of V

for v being Element of V st v in A holds

(l ! A) . v = l . v

let A be Subset of V; :: thesis: for v being Element of V st v in A holds

(l ! A) . v = l . v

let v be Element of V; :: thesis: ( v in A implies (l ! A) . v = l . v )

assume A1: v in A ; :: thesis: (l ! A) . v = l . v

dom (l ! A) = [#] V by FUNCT_2:92;

then A2: (dom (l | A)) \/ (dom ((A `) --> (0. R))) = [#] V by FUNCT_4:def 1;

not v in dom ((A `) --> (0. R)) by A1, XBOOLE_0:def 5;

then (l ! A) . v = (l | A) . v by A2, FUNCT_4:def 1

.= l . v by A1, FUNCT_1:49 ;

hence (l ! A) . v = l . v ; :: thesis: verum

for l being Linear_Combination of V

for A being Subset of V

for v being Element of V st v in A holds

(l ! A) . v = l . v

let V be LeftMod of R; :: thesis: for l being Linear_Combination of V

for A being Subset of V

for v being Element of V st v in A holds

(l ! A) . v = l . v

let l be Linear_Combination of V; :: thesis: for A being Subset of V

for v being Element of V st v in A holds

(l ! A) . v = l . v

let A be Subset of V; :: thesis: for v being Element of V st v in A holds

(l ! A) . v = l . v

let v be Element of V; :: thesis: ( v in A implies (l ! A) . v = l . v )

assume A1: v in A ; :: thesis: (l ! A) . v = l . v

dom (l ! A) = [#] V by FUNCT_2:92;

then A2: (dom (l | A)) \/ (dom ((A `) --> (0. R))) = [#] V by FUNCT_4:def 1;

not v in dom ((A `) --> (0. R)) by A1, XBOOLE_0:def 5;

then (l ! A) . v = (l | A) . v by A2, FUNCT_4:def 1

.= l . v by A1, FUNCT_1:49 ;

hence (l ! A) . v = l . v ; :: thesis: verum