let V be RealLinearSpace; :: thesis: for L1, L2 being Linear_Combination of V holds (vector ((LC_RLSpace V),L1)) - (vector ((LC_RLSpace V),L2)) = L1 - L2

let L1, L2 be Linear_Combination of V; :: thesis: (vector ((LC_RLSpace V),L1)) - (vector ((LC_RLSpace V),L2)) = L1 - L2

- L2 in LinComb V by Def14;

then A1: - L2 in LC_RLSpace V ;

- (vector ((LC_RLSpace V),L2)) = - L2 by Th64

.= vector ((LC_RLSpace V),(- L2)) by A1, Def1 ;

hence (vector ((LC_RLSpace V),L1)) - (vector ((LC_RLSpace V),L2)) = L1 - L2 by Th62; :: thesis: verum

let L1, L2 be Linear_Combination of V; :: thesis: (vector ((LC_RLSpace V),L1)) - (vector ((LC_RLSpace V),L2)) = L1 - L2

- L2 in LinComb V by Def14;

then A1: - L2 in LC_RLSpace V ;

- (vector ((LC_RLSpace V),L2)) = - L2 by Th64

.= vector ((LC_RLSpace V),(- L2)) by A1, Def1 ;

hence (vector ((LC_RLSpace V),L1)) - (vector ((LC_RLSpace V),L2)) = L1 - L2 by Th62; :: thesis: verum