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 by Def12;
then A1: - L2 in LC_CLSpace V ;
- (vector ((LC_CLSpace V),L2)) = - L2 by Th40
.= 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 Th38; :: thesis: verum