let V be non empty CLSStruct ; :: thesis: for L1, L2 being C_Linear_Combination of V holds (vector (LC_CLSpace V),L1) + (vector (LC_CLSpace V),L2) = L1 + L2
let L1, L2 be C_Linear_Combination of V; :: thesis: (vector (LC_CLSpace V),L1) + (vector (LC_CLSpace V),L2) = L1 + L2
set v1 = vector (LC_CLSpace V),L1;
set v2 = vector (LC_CLSpace V),L2;
( L1 in the carrier of (LC_CLSpace V) & L2 in the carrier of (LC_CLSpace V) ) by Def8;
then A1: ( L1 in LC_CLSpace V & L2 in LC_CLSpace V ) by STRUCT_0:def 5;
A2: ( L1 = @ (@ L1) & L2 = @ (@ L2) ) ;
thus (vector (LC_CLSpace V),L1) + (vector (LC_CLSpace V),L2) = (C_LCAdd V) . [L1,(vector (LC_CLSpace V),L2)] by A1, RLVECT_2:def 1
.= (C_LCAdd V) . (@ L1),(@ L2) by A1, RLVECT_2:def 1
.= L1 + L2 by A2, Def9 ; :: thesis: verum