for K being Ring
for r being Scalar of K
for M, N being LeftMod of K
for m, m1, m2 being Vector of M
for n, n1, n2 being Vector of N st M c= N holds
( 0. M = 0. N & ( m1 = n1 & m2 = n2 implies m1 + m2 = n1 + n2 ) & ( m = n implies r * m = r * n ) & ( m = n implies - n = - m ) & ( m1 = n1 & m2 = n2 implies m1 - m2 = n1 - n2 ) & 0. N in M & 0. M in N & ( n1 in M & n2 in M implies n1 + n2 in M ) & ( n in M implies r * n in M ) & ( n in M implies - n in M ) & ( n1 in M & n2 in M implies n1 - n2 in M ) ) by VECTSP_4:11, VECTSP_4:13, VECTSP_4:14, VECTSP_4:15, VECTSP_4:16, VECTSP_4:17, VECTSP_4:19, VECTSP_4:20, VECTSP_4:21, VECTSP_4:22, VECTSP_4:23;