let V be non empty CLSStruct ; :: thesis: for a being Complex
for L being C_Linear_Combination of V holds a * (vector ((LC_CLSpace V),L)) = a * L
let a be Complex; :: thesis: for L being C_Linear_Combination of V holds a * (vector ((LC_CLSpace V),L)) = a * L
let L be C_Linear_Combination of V; :: thesis: a * (vector ((LC_CLSpace V),L)) = a * L
L in the carrier of (LC_CLSpace V) by Def12;
then L in LC_CLSpace V ;
then A1: (C_LCMult V) . [a,(vector ((LC_CLSpace V),L))] = (C_LCMult V) . [a,(@ L)] by RLVECT_2:def 1;
@ (@ L) = L ;
hence a * (vector ((LC_CLSpace V),L)) = a * L by A1, Def16; :: thesis: verum