let R be Ring; :: thesis: for V being LeftMod of R

for L1, L2 being Linear_Combination of V holds (vector ((LC_Z_Module V),L1)) - (vector ((LC_Z_Module V),L2)) = L1 - L2

let V be LeftMod of R; :: thesis: for L1, L2 being Linear_Combination of V holds (vector ((LC_Z_Module V),L1)) - (vector ((LC_Z_Module V),L2)) = L1 - L2

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

- L2 in LinComb V by Def29;

then A1: - L2 in LC_Z_Module V ;

- (vector ((LC_Z_Module V),L2)) = - L2 by Th49

.= vector ((LC_Z_Module V),(- L2)) by A1, RLVECT_2:def 1 ;

hence (vector ((LC_Z_Module V),L1)) - (vector ((LC_Z_Module V),L2)) = L1 - L2 by Th47; :: thesis: verum

for L1, L2 being Linear_Combination of V holds (vector ((LC_Z_Module V),L1)) - (vector ((LC_Z_Module V),L2)) = L1 - L2

let V be LeftMod of R; :: thesis: for L1, L2 being Linear_Combination of V holds (vector ((LC_Z_Module V),L1)) - (vector ((LC_Z_Module V),L2)) = L1 - L2

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

- L2 in LinComb V by Def29;

then A1: - L2 in LC_Z_Module V ;

- (vector ((LC_Z_Module V),L2)) = - L2 by Th49

.= vector ((LC_Z_Module V),(- L2)) by A1, RLVECT_2:def 1 ;

hence (vector ((LC_Z_Module V),L1)) - (vector ((LC_Z_Module V),L2)) = L1 - L2 by Th47; :: thesis: verum