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

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