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 v2 = vector ((LC_CLSpace V),L2);
A1: ( L1 = @ (@ L1) & L2 = @ (@ L2) ) ;
L2 in the carrier of (LC_CLSpace V) by Def12;
then A2: L2 in LC_CLSpace V ;
L1 in the carrier of (LC_CLSpace V) by Def12;
then L1 in LC_CLSpace V ;
hence (vector ((LC_CLSpace V),L1)) + (vector ((LC_CLSpace V),L2)) = (C_LCAdd V) . [L1,(vector ((LC_CLSpace V),L2))] by RLVECT_2:def 1
.= (C_LCAdd V) . ((@ L1),(@ L2)) by A2, RLVECT_2:def 1
.= L1 + L2 by A1, Def15 ;
:: thesis: verum