theorem
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;