let V be RealLinearSpace; :: thesis: for a being Real

for L being Linear_Combination of V holds a * (vector ((LC_RLSpace V),L)) = a * L

let a be Real; :: thesis: for L being Linear_Combination of V holds a * (vector ((LC_RLSpace V),L)) = a * L

let L be Linear_Combination of V; :: thesis: a * (vector ((LC_RLSpace V),L)) = a * L

A1: @ (@ L) = L ;

L in the carrier of (LC_RLSpace V) by Def14;

then L in LC_RLSpace V ;

hence a * (vector ((LC_RLSpace V),L)) = (LCMult V) . [a,(@ L)] by Def1

.= a * L by A1, Def18 ;

:: thesis: verum

for L being Linear_Combination of V holds a * (vector ((LC_RLSpace V),L)) = a * L

let a be Real; :: thesis: for L being Linear_Combination of V holds a * (vector ((LC_RLSpace V),L)) = a * L

let L be Linear_Combination of V; :: thesis: a * (vector ((LC_RLSpace V),L)) = a * L

A1: @ (@ L) = L ;

L in the carrier of (LC_RLSpace V) by Def14;

then L in LC_RLSpace V ;

hence a * (vector ((LC_RLSpace V),L)) = (LCMult V) . [a,(@ L)] by Def1

.= a * L by A1, Def18 ;

:: thesis: verum