let x be set ; :: thesis: for K being Ring
for M1, M2 being LeftMod of K st M1 = VectSpStr(# the carrier of M2, the addF of M2, the ZeroF of M2, the lmult of M2 #) holds
( x in M1 iff x in M2 )
let K be Ring; :: thesis: for M1, M2 being LeftMod of K st M1 = VectSpStr(# the carrier of M2, the addF of M2, the ZeroF of M2, the lmult of M2 #) holds
( x in M1 iff x in M2 )
let M1, M2 be LeftMod of K; :: thesis: ( M1 = VectSpStr(# the carrier of M2, the addF of M2, the ZeroF of M2, the lmult of M2 #) implies ( x in M1 iff x in M2 ) )
A1: ( x in M1 iff x in the carrier of M1 ) by STRUCT_0:def 5;
assume M1 = VectSpStr(# the carrier of M2, the addF of M2, the ZeroF of M2, the lmult of M2 #) ; :: thesis: ( x in M1 iff x in M2 )
hence ( x in M1 iff x in M2 ) by A1, STRUCT_0:def 5; :: thesis: verum