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 Def8;
then L in LC_CLSpace V by STRUCT_0:def 5;
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, Def10; :: thesis: verum