let E, L be Z_Module; for K being Linear_Combination of E
for H being Linear_Combination of L st K = H & ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) holds
Sum K = Sum H
let K be Linear_Combination of E; for H being Linear_Combination of L st K = H & ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) holds
Sum K = Sum H
let H be Linear_Combination of L; ( K = H & ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) implies Sum K = Sum H )
assume AS:
( K = H & ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) )
; Sum K = Sum H
B3:
L is Submodule of E
by AS, LmEMDetX53;
B4:
Carrier K c= the carrier of L
by AS;
H = K | the carrier of L
by AS;
hence
Sum K = Sum H
by ZMODUL03:11, B3, B4; verum