let V be Z_Module; :: thesis: for L being Z_Linear_Combination of V
for a being Integer holds a * (vector ((LC_Z_Module V),L)) = a * L
let L be Z_Linear_Combination of V; :: thesis: for a being Integer holds a * (vector ((LC_Z_Module V),L)) = a * L
let a be Integer; :: 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