begin
theorem Th8:
for
M being
MidSp for
x,
a,
x9 being
Element of
M st
x @ a = x9 @ a holds
x = x9
theorem Th11:
for
M being
MidSp for
a,
b,
c,
d being
Element of
M st
a,
b @@ c,
d holds
c,
d @@ a,
b
theorem Th16:
for
M being
MidSp for
a,
b,
c,
d,
d9 being
Element of
M st
a,
b @@ c,
d &
a,
b @@ c,
d9 holds
d = d9
theorem Th17:
for
M being
MidSp for
x,
y,
a,
b,
c,
d being
Element of
M st
x,
y @@ a,
b &
x,
y @@ c,
d holds
a,
b @@ c,
d
theorem Th18:
for
M being
MidSp for
a,
b,
a9,
b9,
c,
c9 being
Element of
M st
a,
b @@ a9,
b9 &
b,
c @@ b9,
c9 holds
a,
c @@ a9,
c9
definition
let M be
MidSp;
let p,
q be
Element of
[: the carrier of M, the carrier of M:];
reflexivity
for p being Element of [: the carrier of M, the carrier of M:] holds p `1 ,p `2 @@ p `1 ,p `2
by Th14;
symmetry
for p, q being Element of [: the carrier of M, the carrier of M:] st p `1 ,p `2 @@ q `1 ,q `2 holds
q `1 ,q `2 @@ p `1 ,p `2
by Th11;
end;
definition
let M be
MidSp;
let u,
v be
Vector of
M;
existence
ex b1 being Vector of M ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & b1 = [(p `1),(q `2)] ~ )
uniqueness
for b1, b2 being Vector of M st ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & b1 = [(p `1),(q `2)] ~ ) & ex p, q being Element of [: the carrier of M, the carrier of M:] st
( u = p ~ & v = q ~ & p `2 = q `1 & b2 = [(p `1),(q `2)] ~ ) holds
b1 = b2
by Th33;
end;
theorem Th47:
for
M being
MidSp for
u,
v,
w being
Vector of
M st
u + v = u + w holds
v = w