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

for L being Linear_Combination of V

for a being Element of R holds a * (vector ((LC_Z_Module V),L)) = a * L

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

for a being Element of R holds a * (vector ((LC_Z_Module V),L)) = a * L

let L be Linear_Combination of V; :: thesis: for a being Element of R holds a * (vector ((LC_Z_Module V),L)) = a * L

let a be Element of R; :: thesis: a * (vector ((LC_Z_Module V),L)) = a * L

A1: @ (@ L) = L ;

L in the carrier of (LC_Z_Module V) by Def29;

then L in LC_Z_Module V ;

hence a * (vector ((LC_Z_Module V),L)) = (LCMult V) . [a,(@ L)] by RLVECT_2:def 1

.= a * L by A1, Def33 ;

:: thesis: verum

for L being Linear_Combination of V

for a being Element of R holds a * (vector ((LC_Z_Module V),L)) = a * L

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

for a being Element of R holds a * (vector ((LC_Z_Module V),L)) = a * L

let L be Linear_Combination of V; :: thesis: for a being Element of R holds a * (vector ((LC_Z_Module V),L)) = a * L

let a be Element of R; :: thesis: a * (vector ((LC_Z_Module V),L)) = a * L

A1: @ (@ L) = L ;

L in the carrier of (LC_Z_Module V) by Def29;

then L in LC_Z_Module V ;

hence a * (vector ((LC_Z_Module V),L)) = (LCMult V) . [a,(@ L)] by RLVECT_2:def 1

.= a * L by A1, Def33 ;

:: thesis: verum