let L, E be Z_Module; :: thesis: for I being Subset of L

for J being Subset of E st 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 #) & I = J holds

Lin I = Lin J

let I be Subset of L; :: thesis: for J being Subset of E st 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 #) & I = J holds

Lin I = Lin J

let J be Subset of E; :: thesis: ( 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 #) & I = J implies Lin I = Lin J )

assume that

A1: 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 #) and

A2: I = J ; :: thesis: Lin I = Lin J

L is Submodule of E by A1, LmEMDetX53;

hence Lin I = Lin J by A2, ZMODUL03:20; :: thesis: verum

for J being Subset of E st 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 #) & I = J holds

Lin I = Lin J

let I be Subset of L; :: thesis: for J being Subset of E st 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 #) & I = J holds

Lin I = Lin J

let J be Subset of E; :: thesis: ( 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 #) & I = J implies Lin I = Lin J )

assume that

A1: 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 #) and

A2: I = J ; :: thesis: Lin I = Lin J

L is Submodule of E by A1, LmEMDetX53;

hence Lin I = Lin J by A2, ZMODUL03:20; :: thesis: verum