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

set v2 = vector ((LC_Z_Module V),L2);

A1: ( L1 = @ (@ L1) & L2 = @ (@ L2) ) ;

L2 in the carrier of (LC_Z_Module V) by Def29;

then A2: L2 in LC_Z_Module V ;

L1 in the carrier of (LC_Z_Module V) by Def29;

then L1 in LC_Z_Module V ;

hence (vector ((LC_Z_Module V),L1)) + (vector ((LC_Z_Module V),L2)) = (LCAdd V) . [L1,(vector ((LC_Z_Module V),L2))] by RLVECT_2:def 1

.= (LCAdd V) . ((@ L1),(@ L2)) by A2, RLVECT_2:def 1

.= L1 + L2 by A1, Def32 ;

:: 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

set v2 = vector ((LC_Z_Module V),L2);

A1: ( L1 = @ (@ L1) & L2 = @ (@ L2) ) ;

L2 in the carrier of (LC_Z_Module V) by Def29;

then A2: L2 in LC_Z_Module V ;

L1 in the carrier of (LC_Z_Module V) by Def29;

then L1 in LC_Z_Module V ;

hence (vector ((LC_Z_Module V),L1)) + (vector ((LC_Z_Module V),L2)) = (LCAdd V) . [L1,(vector ((LC_Z_Module V),L2))] by RLVECT_2:def 1

.= (LCAdd V) . ((@ L1),(@ L2)) by A2, RLVECT_2:def 1

.= L1 + L2 by A1, Def32 ;

:: thesis: verum