theorem :: ZMODLAT2:31

for E, L being 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
Carrier K = Carrier H ;