for K being Ring
for M1, M2, N being LeftMod of K st M1 c= N & M2 c= N holds
( 0. M1 = 0. M2 & 0. M1 in M2 & ( the carrier of M1 c= the carrier of M2 implies M1 c= M2 ) & ( ( for n being Vector of N st n in M1 holds
n in M2 ) implies M1 c= M2 ) & ( the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 ) & (0). M1 c= M2 ) by VECTSP_4:12, VECTSP_4:18, VECTSP_4:27, VECTSP_4:28, VECTSP_4:29, VECTSP_4:40;