begin
begin
begin
begin
begin
theorem
for
K being
Ring for
r being
Scalar of
K for
M,
N being
LeftMod of
K for
m1,
m2,
m being
Vector of
M for
n1,
n2,
n 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 ) )