let E, L be Z_Module; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 #) ) ; :: thesis: 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; :: thesis: verum