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 M' = M as Subspace of N by A1, Def7;
0. M' = 0. N by VECTSP_4:19;
hence 0. M = 0. N ; :: thesis:

end;

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

proof

assume A2: ( m1 = n1 & m2 = n2 ) ; :: thesis:
reconsider M' = M as Subspace of N by A1, Def7;
reconsider m1' = m1, m2' = m2 as Vector of M' ;
( m1' = n1 & m2' = n2 ) by A2;
hence m1 + m2 = n1 + n2 by VECTSP_4:21; :: thesis:

end;

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

proof

assume A3: m = n ; :: thesis:
reconsider M' = M as Subspace of N by A1, Def7;
reconsider m' = m as Vector of M' ;
m' = n by A3;
hence r * m = r * n by VECTSP_4:22; :: thesis:

end;

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

proof

assume A4: m = n ; :: thesis:
reconsider M' = M as Subspace of N by A1, Def7;
reconsider m' = m as Vector of M' ;
m' = n by A4;
hence - n = - m by VECTSP_4:23; :: thesis:

end;

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

proof

assume A5: ( m1 = n1 & m2 = n2 ) ; :: thesis:
reconsider M' = M as Subspace of N by A1, Def7;
reconsider m1' = m1, m2' = m2 as Vector of M' ;
( m1' = n1 & m2' = n2 ) by A5;
hence m1 - m2 = n1 - n2 by VECTSP_4:24; :: thesis:

end;

thus 0. N in M :: thesis:

proof

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

end;

thus 0. M in N :: thesis:

proof

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

end;

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

proof

assume A6: ( n1 in M & n2 in M ) ; :: thesis:
reconsider M' = M as Subspace of N by A1, Def7;
( n1 in M' & n2 in M' ) by A6;
hence n1 + n2 in M by VECTSP_4:28; :: thesis:

end;

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

proof

assume A7: n in M ; :: thesis:
reconsider M' = M as Subspace of N by A1, Def7;
n in M' by A7;
hence r * n in M by VECTSP_4:29; :: thesis:

end;

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

proof

assume A8: n in M ; :: thesis:
reconsider M' = M as Subspace of N by A1, Def7;
n in M' by A8;
hence - n in M by VECTSP_4:30; :: thesis:

end;

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

proof

assume A9: ( n1 in M & n2 in M ) ; :: thesis:
reconsider M' = M as Subspace of N by A1, Def7;
( n1 in M' & n2 in M' ) by A9;
hence n1 - n2 in M by VECTSP_4:31; :: thesis:

end;