environ
vocabularies HIDDEN, STRUCT_0, BINOP_1, XBOOLE_0, SUBSET_1, QC_LANG1, FUNCT_1, FUNCT_5, ZFMISC_1, MCART_1, RELAT_1, VECTSP_1, ARYTM_3, ARYTM_1, ALGSTR_0, SUPINF_2, RLVECT_1, MIDSP_1, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, MCART_1, DOMAIN_1, ORDINAL1, FUNCT_2, FUNCT_5, STRUCT_0, ALGSTR_0, RLVECT_1;
definitions STRUCT_0, RLVECT_1, ALGSTR_0;
theorems FUNCT_2, TARSKI, BINOP_1;
schemes FUNCT_2, BINOP_1;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, RELAT_1, XTUPLE_0;
constructors HIDDEN, BINOP_1, DOMAIN_1, RLVECT_1, FUNCT_5, RELSET_1, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE;
equalities STRUCT_0, ALGSTR_0, ORDINAL1;
expansions ;
theorem Th8:
for
M being
MidSp for
a,
x,
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 by Th8;
theorem Th17:
for
M being
MidSp for
a,
b,
c,
d,
x,
y 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,
c,
a9,
b9,
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
;
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
;
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