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
( - L2 in C_LinComb V & the carrier of (LC_CLSpace V) = C_LinComb V ) by Def8;
then A1: - L2 in LC_CLSpace V by STRUCT_0:def 5;
- (vector (LC_CLSpace V),L2) = - L2 by Th98
.= vector (LC_CLSpace V),(- L2) by A1, RLVECT_2:def 1 ;
hence (vector (LC_CLSpace V),L1) - (vector (LC_CLSpace V),L2) = L1 - L2 by Th96; :: thesis: verum