theorem LmEMDetX541: :: ZMODLAT2:30

for E, L being Z_Module
for I being Subset of L
for J being Subset of E
for K being Linear_Combination of J st I = J & 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
K is Linear_Combination of I