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
L in the carrier of (LC_RLSpace V) by Def16;
then A1: L in LC_RLSpace V by STRUCT_0:def 5;
A2: @ (@ L) = L ;
thus a * (vector (LC_RLSpace V),L) = (LCMult V) . [a,(@ L)] by A1, Def1
.= a * L by A2, Def20 ; :: thesis: verum