let K be Ring; :: thesis:
let r be Scalar of K; :: thesis:
let M, N be LeftMod of K; :: thesis:
let m1, m2, m be Vector of M; :: thesis:
let n1, n2, n be Vector of N; :: thesis:
assume A1: M c= N ; :: thesis:
thus 0. M = 0. N :: thesis:

proof

reconsider M9 = M as Subspace of N by A1, Def7;
0. M9 = 0. N by VECTSP_4:11;
hence 0. M = 0. N ; :: thesis:

end;

thus ( m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2 ) :: thesis:

proof

reconsider M9 = M as Subspace of N by A1, Def7;
assume that
A2: m1 = n1 and
A3: m2 = n2 ; :: thesis:
reconsider m19 = m1 as Vector of M9 ;
m19 = n1 by A2;
hence m1 + m2 = n1 + n2 by A3, VECTSP_4:13; :: thesis:

end;

thus ( m = n implies r * m = r * n ) :: thesis:

proof

reconsider M9 = M as Subspace of N by A1, Def7;
reconsider m9 = m as Vector of M9 ;
assume m = n ; :: thesis:
then m9 = n ;
hence r * m = r * n by VECTSP_4:14; :: thesis:

end;

thus ( m = n implies - n = - m ) :: thesis:

proof

reconsider M9 = M as Subspace of N by A1, Def7;
reconsider m9 = m as Vector of M9 ;
assume m = n ; :: thesis:
then m9 = n ;
hence - n = - m by VECTSP_4:15; :: thesis:

end;

thus ( m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 ) :: thesis:

proof

reconsider M9 = M as Subspace of N by A1, Def7;
assume that
A4: m1 = n1 and
A5: m2 = n2 ; :: thesis:
reconsider m19 = m1 as Vector of M9 ;
m19 = n1 by A4;
hence m1 - m2 = n1 - n2 by A5, VECTSP_4:16; :: thesis:

end;

thus 0. N in M :: thesis:

proof

reconsider M9 = M as Subspace of N by A1, Def7;
0. N in M9 by VECTSP_4:17;
hence 0. N in M ; :: thesis:

end;

thus 0. M in N :: thesis:

proof

reconsider M9 = M as Subspace of N by A1, Def7;
0. M9 in N by VECTSP_4:19;
hence 0. M in N ; :: thesis:

end;

thus ( n1 in M & n2 in M implies n1 + n2 in M ) :: thesis:

proof

reconsider M9 = M as Subspace of N by A1, Def7;
assume that
A6: n1 in M and
A7: n2 in M ; :: thesis:
n1 in M9 by A6;
hence n1 + n2 in M by A7, VECTSP_4:20; :: thesis:

end;

thus ( n in M implies r * n in M ) :: thesis:

proof

reconsider M9 = M as Subspace of N by A1, Def7;
assume n in M ; :: thesis:
then n in M9 ;
hence r * n in M by VECTSP_4:21; :: thesis:

end;

thus ( n in M implies - n in M ) :: thesis:

proof

reconsider M9 = M as Subspace of N by A1, Def7;
assume n in M ; :: thesis:
then n in M9 ;
hence - n in M by VECTSP_4:22; :: thesis:

end;

thus ( n1 in M & n2 in M implies n1 - n2 in M ) :: thesis:

proof

reconsider M9 = M as Subspace of N by A1, Def7;
assume that
A8: n1 in M and
A9: n2 in M ; :: thesis:
n1 in M9 by A8;
hence n1 - n2 in M by A9, VECTSP_4:23; :: thesis:

end;