let K be Ring; :: thesis:
let M1, N, M2 be LeftMod of K; :: thesis:
assume that
A1: M1 c= N and
A2: M2 c= N ; :: thesis:
thus 0. M1 = 0. M2 :: thesis:

proof

reconsider M19 = M1, M29 = M2 as Subspace of N by A1, A2, Def7;
0. M19 = 0. M29 by VECTSP_4:12;
hence 0. M1 = 0. M2 ; :: thesis:

end;

thus 0. M1 in M2 :: thesis:

proof

reconsider M19 = M1, M29 = M2 as Subspace of N by A1, A2, Def7;
0. M19 in M29 by VECTSP_4:18;
hence 0. M1 in M2 ; :: thesis:

end;

thus ( the carrier of M1 c= the carrier of M2 implies M1 c= M2 ) :: thesis:

proof

reconsider M19 = M1, M29 = M2 as Subspace of N by A1, A2, Def7;
assume the carrier of M1 c= the carrier of M2 ; :: thesis:
then M19 is Subspace of M29 by VECTSP_4:27;
hence M1 c= M2 by Def7; :: thesis:

end;

thus ( ( for n being Vector of N st n in M1 holds
n in M2 ) implies M1 c= M2 ) :: thesis:

proof

reconsider M19 = M1, M29 = M2 as Subspace of N by A1, A2, Def7;
assume for n being Vector of N st n in M1 holds
n in M2 ; :: thesis:
then M19 is Subspace of M29 by VECTSP_4:28;
hence M1 c= M2 by Def7; :: thesis:

end;

thus ( the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 ) :: thesis:

proof

assume that
A3: the carrier of M1 = the carrier of M2 and
A4: M1 is strict and
A5: M2 is strict ; :: thesis:
reconsider M29 = M2 as strict Subspace of N by A2, A5, Def7;
reconsider M19 = M1 as strict Subspace of N by A1, A4, Def7;
M19 = M29 by A3, VECTSP_4:29;
hence M1 = M2 ; :: thesis:

end;

thus (0). M1 c= M2 :: thesis:

proof

reconsider M19 = M1, M29 = M2 as Subspace of N by A1, A2, Def7;
(0). M19 is Subspace of M29 by VECTSP_4:40;
hence (0). M1 c= M2 by Def7; :: thesis:

end;