:: METRIC_1 semantic presentation

REAL is non empty V36() V71() V72() V73() V77() set
NAT is V71() V72() V73() V74() V75() V76() V77() Element of bool REAL

RAT is non empty V36() V71() V72() V73() V74() V77() set

1 is non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT
{{},1} is non empty set
COMPLEX is non empty V36() V71() V77() set
omega is V71() V72() V73() V74() V75() V76() V77() set

INT is non empty V36() V71() V72() V73() V74() V75() V77() set

bool [:1,1:] is set

bool [:[:1,1:],1:] is set

the non empty set is non empty set
[: the non empty set , the non empty set :] is Relation-like set
[:[: the non empty set , the non empty set :],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the non empty set , the non empty set :],REAL:] is set
the Relation-like [: the non empty set , the non empty set :] -defined REAL -valued Function-like total V18([: the non empty set , the non empty set :], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the non empty set , the non empty set :],REAL:] is Relation-like [: the non empty set , the non empty set :] -defined REAL -valued Function-like total V18([: the non empty set , the non empty set :], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the non empty set , the non empty set :],REAL:]
( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined REAL -valued Function-like total V18([: the non empty set , the non empty set :], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the non empty set , the non empty set :],REAL:]) is () ()
the carrier of ( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined REAL -valued Function-like total V18([: the non empty set , the non empty set :], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the non empty set , the non empty set :],REAL:]) is set
M0 is set
M is set
[:M0,M:] is Relation-like set

bool [:[:M0,M:],REAL:] is set

r is Element of M0
x is Element of M
p . (r,x) is set
[r,x] is set
p . [r,x] is ext-real V34() real set

M0 is ()
the carrier of M0 is set
the of M0 is Relation-like [: the carrier of M0, the carrier of M0:] -defined REAL -valued Function-like total V18([: the carrier of M0, the carrier of M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M0, the carrier of M0:],REAL:]
[: the carrier of M0, the carrier of M0:] is Relation-like set
[:[: the carrier of M0, the carrier of M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M0, the carrier of M0:],REAL:] is set
M is Element of the carrier of M0
p is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
op2 is set

bool [:[:1,1:],REAL:] is set

op2 . ({},{}) is set
is set

M0 is ext-real natural V34() real V59() V60() Element of 1
M is ext-real natural V34() real V59() V60() Element of 1
op2 . (M0,M) is ext-real natural V34() real V59() V60() Element of 1
[M0,M] is set
op2 . [M0,M] is ext-real natural V34() real set
M0 is ext-real natural V34() real V59() V60() Element of 1
M is ext-real natural V34() real V59() V60() Element of 1
op2 . (M0,M) is ext-real natural V34() real V59() V60() Element of 1
[M0,M] is set
op2 . [M0,M] is ext-real natural V34() real set
op2 . (M,M0) is ext-real natural V34() real V59() V60() Element of 1
[M,M0] is set
op2 . [M,M0] is ext-real natural V34() real set

M is set
p is set
M0 . (M,p) is set
[M,p] is set
M0 . [M,p] is ext-real natural V34() real V60() set
M0 is ext-real natural V34() real V59() V60() Element of 1
p is ext-real natural V34() real V59() V60() Element of 1
op2 . (M0,p) is ext-real natural V34() real V59() V60() Element of 1
[M0,p] is set
op2 . [M0,p] is ext-real natural V34() real V60() set
M is ext-real natural V34() real V59() V60() Element of 1
op2 . (M0,M) is ext-real natural V34() real V59() V60() Element of 1
[M0,M] is set
op2 . [M0,M] is ext-real natural V34() real V60() set
op2 . (M,p) is ext-real natural V34() real V59() V60() Element of 1
[M,p] is set
op2 . [M,p] is ext-real natural V34() real V60() set
(op2 . (M0,M)) + (op2 . (M,p)) is ext-real V34() real set
M0 is set
[:M0,M0:] is Relation-like set

bool [:[:M0,M0:],REAL:] is set

(1,()) is () ()
M0 is non empty () ()
the carrier of M0 is non empty set
the of M0 is Relation-like [: the carrier of M0, the carrier of M0:] -defined REAL -valued Function-like total V18([: the carrier of M0, the carrier of M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M0, the carrier of M0:],REAL:]
[: the carrier of M0, the carrier of M0:] is Relation-like set
[:[: the carrier of M0, the carrier of M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M0, the carrier of M0:],REAL:] is set
M is Element of the carrier of M0
p is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
M is Element of the carrier of M0
p is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
( the carrier of M0, the carrier of M0, the of M0,p,M) is ext-real V34() real Element of REAL
[p,M] is set
the of M0 . [p,M] is ext-real V34() real set
M is Element of the carrier of M0
r is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,r) is ext-real V34() real Element of REAL
[M,r] is set
the of M0 . [M,r] is ext-real V34() real set
p is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
( the carrier of M0, the carrier of M0, the of M0,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M0 . [p,r] is ext-real V34() real set
( the carrier of M0, the carrier of M0, the of M0,M,p) + ( the carrier of M0, the carrier of M0, the of M0,p,r) is ext-real V34() real Element of REAL
M is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,M) is ext-real V34() real Element of REAL
[M,M] is set
the of M0 . [M,M] is ext-real V34() real set
M0 is ()
the carrier of M0 is set
the of M0 is Relation-like [: the carrier of M0, the carrier of M0:] -defined REAL -valued Function-like total V18([: the carrier of M0, the carrier of M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M0, the carrier of M0:],REAL:]
[: the carrier of M0, the carrier of M0:] is Relation-like set
[:[: the carrier of M0, the carrier of M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M0, the carrier of M0:],REAL:] is set
M is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,M) is ext-real V34() real Element of REAL
[M,M] is set
the of M0 . [M,M] is ext-real V34() real set
(M0,M,M) is ext-real V34() real Element of REAL
M is Element of the carrier of M0
(M0,M,M) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,M,M) is ext-real V34() real Element of REAL
[M,M] is set
the of M0 . [M,M] is ext-real V34() real set
M0 is ()
the carrier of M0 is set
the of M0 is Relation-like [: the carrier of M0, the carrier of M0:] -defined REAL -valued Function-like total V18([: the carrier of M0, the carrier of M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M0, the carrier of M0:],REAL:]
[: the carrier of M0, the carrier of M0:] is Relation-like set
[:[: the carrier of M0, the carrier of M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M0, the carrier of M0:],REAL:] is set
M is Element of the carrier of M0
p is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
(M0,M,p) is ext-real V34() real Element of REAL
M is Element of the carrier of M0
p is Element of the carrier of M0
(M0,M,p) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
M0 is ()
the carrier of M0 is set
the of M0 is Relation-like [: the carrier of M0, the carrier of M0:] -defined REAL -valued Function-like total V18([: the carrier of M0, the carrier of M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M0, the carrier of M0:],REAL:]
[: the carrier of M0, the carrier of M0:] is Relation-like set
[:[: the carrier of M0, the carrier of M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M0, the carrier of M0:],REAL:] is set
M is Element of the carrier of M0
p is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
( the carrier of M0, the carrier of M0, the of M0,p,M) is ext-real V34() real Element of REAL
[p,M] is set
the of M0 . [p,M] is ext-real V34() real set
(M0,M,p) is ext-real V34() real Element of REAL
(M0,p,M) is ext-real V34() real Element of REAL
M0 is ()
the carrier of M0 is set
the of M0 is Relation-like [: the carrier of M0, the carrier of M0:] -defined REAL -valued Function-like total V18([: the carrier of M0, the carrier of M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M0, the carrier of M0:],REAL:]
[: the carrier of M0, the carrier of M0:] is Relation-like set
[:[: the carrier of M0, the carrier of M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M0, the carrier of M0:],REAL:] is set
M is Element of the carrier of M0
r is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,r) is ext-real V34() real Element of REAL
[M,r] is set
the of M0 . [M,r] is ext-real V34() real set
p is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
( the carrier of M0, the carrier of M0, the of M0,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M0 . [p,r] is ext-real V34() real set
( the carrier of M0, the carrier of M0, the of M0,M,p) + ( the carrier of M0, the carrier of M0, the of M0,p,r) is ext-real V34() real Element of REAL
(M0,p,r) is ext-real V34() real Element of REAL
(M0,M,p) is ext-real V34() real Element of REAL
(M0,M,r) is ext-real V34() real Element of REAL
M is Element of the carrier of M0
r is Element of the carrier of M0
(M0,M,r) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,M,r) is ext-real V34() real Element of REAL
[M,r] is set
the of M0 . [M,r] is ext-real V34() real set
p is Element of the carrier of M0
(M0,M,p) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
(M0,p,r) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M0 . [p,r] is ext-real V34() real set
(M0,M,p) + (M0,p,r) is ext-real V34() real Element of REAL
M0 is () ()
the carrier of M0 is set
the of M0 is Relation-like [: the carrier of M0, the carrier of M0:] -defined REAL -valued Function-like total V18([: the carrier of M0, the carrier of M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M0, the carrier of M0:],REAL:]
[: the carrier of M0, the carrier of M0:] is Relation-like set
[:[: the carrier of M0, the carrier of M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M0, the carrier of M0:],REAL:] is set
r is Element of the carrier of M0
x is Element of the carrier of M0
(M0,r,x) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,r,x) is ext-real V34() real Element of REAL
[r,x] is set
the of M0 . [r,x] is ext-real V34() real set
(M0,x,r) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,x,r) is ext-real V34() real Element of REAL
[x,r] is set
the of M0 . [x,r] is ext-real V34() real set
M0 is () () () ()
the carrier of M0 is set
M is Element of the carrier of M0
p is Element of the carrier of M0
(M0,M,p) is ext-real V34() real Element of REAL
the of M0 is Relation-like [: the carrier of M0, the carrier of M0:] -defined REAL -valued Function-like total V18([: the carrier of M0, the carrier of M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M0, the carrier of M0:],REAL:]
[: the carrier of M0, the carrier of M0:] is Relation-like set
[:[: the carrier of M0, the carrier of M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M0, the carrier of M0:],REAL:] is set
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
2 is non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT
1 / 2 is ext-real V34() real Element of REAL
(M0,M,M) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,M,M) is ext-real V34() real Element of REAL
[M,M] is set
the of M0 . [M,M] is ext-real V34() real set
(1 / 2) * (M0,M,M) is ext-real V34() real Element of REAL
(1 / 2) * 0 is ext-real V34() real Element of REAL
(M0,p,M) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,p,M) is ext-real V34() real Element of REAL
[p,M] is set
the of M0 . [p,M] is ext-real V34() real set
(M0,M,p) + (M0,p,M) is ext-real V34() real Element of REAL
1 * (M0,M,p) is ext-real V34() real Element of REAL
(1 * (M0,M,p)) + (1 * (M0,M,p)) is ext-real V34() real Element of REAL
(1 / 2) * ((1 * (M0,M,p)) + (1 * (M0,M,p))) is ext-real V34() real Element of REAL
M0 is ()
the carrier of M0 is set
the of M0 is Relation-like [: the carrier of M0, the carrier of M0:] -defined REAL -valued Function-like total V18([: the carrier of M0, the carrier of M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M0, the carrier of M0:],REAL:]
[: the carrier of M0, the carrier of M0:] is Relation-like set
[:[: the carrier of M0, the carrier of M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M0, the carrier of M0:],REAL:] is set
M is Element of the carrier of M0
p is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
( the carrier of M0, the carrier of M0, the of M0,p,M) is ext-real V34() real Element of REAL
[p,M] is set
the of M0 . [p,M] is ext-real V34() real set
(M0,M,p) is ext-real V34() real Element of REAL
(M0,p,M) is ext-real V34() real Element of REAL
M is Element of the carrier of M0
r is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,r) is ext-real V34() real Element of REAL
[M,r] is set
the of M0 . [M,r] is ext-real V34() real set
p is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
( the carrier of M0, the carrier of M0, the of M0,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M0 . [p,r] is ext-real V34() real set
( the carrier of M0, the carrier of M0, the of M0,M,p) + ( the carrier of M0, the carrier of M0, the of M0,p,r) is ext-real V34() real Element of REAL
(M0,p,r) is ext-real V34() real Element of REAL
(M0,M,r) is ext-real V34() real Element of REAL
(M0,M,p) is ext-real V34() real Element of REAL
M is Element of the carrier of M0
p is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
(M0,M,p) is ext-real V34() real Element of REAL
M is Element of the carrier of M0
( the carrier of M0, the carrier of M0, the of M0,M,M) is ext-real V34() real Element of REAL
[M,M] is set
the of M0 . [M,M] is ext-real V34() real set
(M0,M,M) is ext-real V34() real Element of REAL
M0 is () () () () ()
the carrier of M0 is set
M is Element of the carrier of M0
p is Element of the carrier of M0
(M0,M,p) is ext-real V34() real Element of REAL
the of M0 is Relation-like [: the carrier of M0, the carrier of M0:] -defined REAL -valued Function-like total V18([: the carrier of M0, the carrier of M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M0, the carrier of M0:],REAL:]
[: the carrier of M0, the carrier of M0:] is Relation-like set
[:[: the carrier of M0, the carrier of M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M0, the carrier of M0:],REAL:] is set
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
M0 is set
[:M0,M0:] is Relation-like set

bool [:[:M0,M0:],REAL:] is set

p is Element of M0
(M0,M0,M,p,p) is ext-real V34() real Element of REAL
[p,p] is set
M . [p,p] is ext-real V34() real set
r is Element of M0
(M0,M0,M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
M . [p,r] is ext-real V34() real set
{0,1} is non empty V71() V72() V73() V74() V75() V76() set
id M0 is Relation-like M0 -defined M0 -valued Function-like one-to-one total V18(M0,M0) Element of bool [:M0,M0:]
bool [:M0,M0:] is set
[:M0,M0:] \ (id M0) is Relation-like M0 -defined M0 -valued Element of bool [:M0,M0:]
chi (([:M0,M0:] \ (id M0)),[:M0,M0:]) is Relation-like [:M0,M0:] -defined {{},1} -valued Function-like total V18([:M0,M0:],{{},1}) Element of bool [:[:M0,M0:],{{},1}:]
[:[:M0,M0:],{{},1}:] is Relation-like set
bool [:[:M0,M0:],{{},1}:] is set
rng (chi (([:M0,M0:] \ (id M0)),[:M0,M0:])) is set
dom (chi (([:M0,M0:] \ (id M0)),[:M0,M0:])) is Relation-like set

p is Element of M0
(M0,M0,M,p,p) is ext-real V34() real Element of REAL
[p,p] is set
M . [p,p] is ext-real V34() real set
r is Element of M0
(M0,M0,M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
M . [p,r] is ext-real V34() real set
[:M0,M0:] \ ([:M0,M0:] \ (id M0)) is Relation-like M0 -defined M0 -valued Element of bool [:M0,M0:]
[:M0,M0:] /\ (id M0) is Relation-like M0 -defined M0 -valued Element of bool [:M0,M0:]

r is Element of M0
x is Element of M0
(M0,M0,M,r,x) is ext-real V34() real Element of REAL
[r,x] is set
M . [r,x] is ext-real V34() real set
(M0,M0,p,r,x) is ext-real V34() real Element of REAL
p . [r,x] is ext-real V34() real set
r is Element of M0
x is Element of M0
(M0,M0,M,r,x) is ext-real V34() real Element of REAL
[r,x] is set
M . [r,x] is ext-real V34() real set
(M0,M0,p,r,x) is ext-real V34() real Element of REAL
p . [r,x] is ext-real V34() real set
r is Element of M0
x is Element of M0
(M0,M0,M,r,x) is ext-real V34() real Element of REAL
[r,x] is set
M . [r,x] is ext-real V34() real set
(M0,M0,p,r,x) is ext-real V34() real Element of REAL
p . [r,x] is ext-real V34() real set
r is Element of M0
x is Element of M0
(M0,M0,M,r,x) is ext-real V34() real Element of REAL
[r,x] is set
M . [r,x] is ext-real V34() real set
(M0,M0,p,r,x) is ext-real V34() real Element of REAL
p . [r,x] is ext-real V34() real set
M0 is set

[:M0,M0:] is Relation-like set

bool [:[:M0,M0:],REAL:] is set
(M0,(M0)) is () ()
M0 is non empty set
(M0) is () ()

[:M0,M0:] is Relation-like set

bool [:[:M0,M0:],REAL:] is set
(M0,(M0)) is () ()
M0 is set
(M0) is () ()

[:M0,M0:] is Relation-like set

bool [:[:M0,M0:],REAL:] is set
(M0,(M0)) is () ()
the carrier of (M0,(M0)) is set
the of (M0,(M0)) is Relation-like [: the carrier of (M0,(M0)), the carrier of (M0,(M0)):] -defined REAL -valued Function-like total V18([: the carrier of (M0,(M0)), the carrier of (M0,(M0)):], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of (M0,(M0)), the carrier of (M0,(M0)):],REAL:]
[: the carrier of (M0,(M0)), the carrier of (M0,(M0)):] is Relation-like set
[:[: the carrier of (M0,(M0)), the carrier of (M0,(M0)):],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of (M0,(M0)), the carrier of (M0,(M0)):],REAL:] is set
p is Element of the carrier of (M0,(M0))
r is Element of the carrier of (M0,(M0))
( the carrier of (M0,(M0)), the carrier of (M0,(M0)), the of (M0,(M0)),p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of (M0,(M0)) . [p,r] is ext-real V34() real set
p is Element of the carrier of (M0,(M0))
r is Element of the carrier of (M0,(M0))
( the carrier of (M0,(M0)), the carrier of (M0,(M0)), the of (M0,(M0)),p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of (M0,(M0)) . [p,r] is ext-real V34() real set
( the carrier of (M0,(M0)), the carrier of (M0,(M0)), the of (M0,(M0)),r,p) is ext-real V34() real Element of REAL
[r,p] is set
the of (M0,(M0)) . [r,p] is ext-real V34() real set
p is Element of the carrier of (M0,(M0))
x is Element of the carrier of (M0,(M0))
( the carrier of (M0,(M0)), the carrier of (M0,(M0)), the of (M0,(M0)),p,x) is ext-real V34() real Element of REAL
[p,x] is set
the of (M0,(M0)) . [p,x] is ext-real V34() real set
r is Element of the carrier of (M0,(M0))
( the carrier of (M0,(M0)), the carrier of (M0,(M0)), the of (M0,(M0)),p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of (M0,(M0)) . [p,r] is ext-real V34() real set
( the carrier of (M0,(M0)), the carrier of (M0,(M0)), the of (M0,(M0)),r,x) is ext-real V34() real Element of REAL
[r,x] is set
the of (M0,(M0)) . [r,x] is ext-real V34() real set
( the carrier of (M0,(M0)), the carrier of (M0,(M0)), the of (M0,(M0)),p,r) + ( the carrier of (M0,(M0)), the carrier of (M0,(M0)), the of (M0,(M0)),r,x) is ext-real V34() real Element of REAL
p is Element of the carrier of (M0,(M0))
( the carrier of (M0,(M0)), the carrier of (M0,(M0)), the of (M0,(M0)),p,p) is ext-real V34() real Element of REAL
[p,p] is set
the of (M0,(M0)) . [p,p] is ext-real V34() real set

M is ext-real V34() real Element of REAL
p is ext-real V34() real Element of REAL
(REAL,REAL,M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
M0 . [M,p] is ext-real V34() real set
M - p is ext-real V34() real Element of REAL
abs (M - p) is ext-real V34() real Element of REAL

p is ext-real V34() real Element of REAL
r is ext-real V34() real Element of REAL
(REAL,REAL,M0,p,r) is ext-real V34() real Element of REAL
[p,r] is set
M0 . [p,r] is ext-real V34() real set
(REAL,REAL,M,p,r) is ext-real V34() real Element of REAL
M . [p,r] is ext-real V34() real set
p - r is ext-real V34() real Element of REAL
abs (p - r) is ext-real V34() real Element of REAL

M0 is ext-real V34() real Element of REAL
M is ext-real V34() real Element of REAL
(REAL,REAL,(),M0,M) is ext-real V34() real Element of REAL
[M0,M] is set
() . [M0,M] is ext-real V34() real set
M0 - M is ext-real V34() real Element of REAL
abs (M0 - M) is ext-real V34() real Element of REAL
M0 - M is ext-real V34() real Element of REAL
abs (M0 - M) is ext-real V34() real Element of REAL
M0 is ext-real V34() real Element of REAL
M is ext-real V34() real Element of REAL
(REAL,REAL,(),M0,M) is ext-real V34() real Element of REAL
[M0,M] is set
() . [M0,M] is ext-real V34() real set
(REAL,REAL,(),M,M0) is ext-real V34() real Element of REAL
[M,M0] is set
() . [M,M0] is ext-real V34() real set
M0 - M is ext-real V34() real Element of REAL
abs (M0 - M) is ext-real V34() real Element of REAL
- (M0 - M) is ext-real V34() real Element of REAL
abs (- (M0 - M)) is ext-real V34() real Element of REAL
M - M0 is ext-real V34() real Element of REAL
abs (M - M0) is ext-real V34() real Element of REAL
M0 is ext-real V34() real Element of REAL
M is ext-real V34() real Element of REAL
(REAL,REAL,(),M0,M) is ext-real V34() real Element of REAL
[M0,M] is set
() . [M0,M] is ext-real V34() real set
p is ext-real V34() real Element of REAL
(REAL,REAL,(),M0,p) is ext-real V34() real Element of REAL
[M0,p] is set
() . [M0,p] is ext-real V34() real set
(REAL,REAL,(),p,M) is ext-real V34() real Element of REAL
[p,M] is set
() . [p,M] is ext-real V34() real set
(REAL,REAL,(),M0,p) + (REAL,REAL,(),p,M) is ext-real V34() real Element of REAL
M0 - M is ext-real V34() real Element of REAL
abs (M0 - M) is ext-real V34() real Element of REAL
M0 - p is ext-real V34() real Element of REAL
p - M is ext-real V34() real Element of REAL
(M0 - p) + (p - M) is ext-real V34() real Element of REAL
abs ((M0 - p) + (p - M)) is ext-real V34() real Element of REAL
abs (M0 - p) is ext-real V34() real Element of REAL
abs (p - M) is ext-real V34() real Element of REAL
(abs (M0 - p)) + (abs (p - M)) is ext-real V34() real Element of REAL
(REAL,()) is () ()
() is () ()
M0 is non empty ()
the carrier of M0 is non empty set
M is Element of the carrier of M0
p is Element of the carrier of M0
(M0,M,p) is ext-real V34() real Element of REAL
the of M0 is Relation-like [: the carrier of M0, the carrier of M0:] -defined REAL -valued Function-like total V18([: the carrier of M0, the carrier of M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M0, the carrier of M0:],REAL:]
[: the carrier of M0, the carrier of M0:] is Relation-like set
[:[: the carrier of M0, the carrier of M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M0, the carrier of M0:],REAL:] is set
( the carrier of M0, the carrier of M0, the of M0,M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of M0 . [M,p] is ext-real V34() real set
r is Element of the carrier of M0
x is Element of the carrier of M0
(M0,r,x) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,r,x) is ext-real V34() real Element of REAL
[r,x] is set
the of M0 . [r,x] is ext-real V34() real set
s is Element of the carrier of M0
X is Element of the carrier of M0
(M0,s,X) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,s,X) is ext-real V34() real Element of REAL
[s,X] is set
the of M0 . [s,X] is ext-real V34() real set
(M0,X,s) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,X,s) is ext-real V34() real Element of REAL
[X,s] is set
the of M0 . [X,s] is ext-real V34() real set
X is Element of the carrier of M0
c10 is Element of the carrier of M0
(M0,X,c10) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,X,c10) is ext-real V34() real Element of REAL
[X,c10] is set
the of M0 . [X,c10] is ext-real V34() real set
c9 is Element of the carrier of M0
(M0,X,c9) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,X,c9) is ext-real V34() real Element of REAL
[X,c9] is set
the of M0 . [X,c9] is ext-real V34() real set
(M0,c9,c10) is ext-real V34() real Element of REAL
( the carrier of M0, the carrier of M0, the of M0,c9,c10) is ext-real V34() real Element of REAL
[c9,c10] is set
the of M0 . [c9,c10] is ext-real V34() real set
(M0,X,c9) + (M0,c9,c10) is ext-real V34() real Element of REAL
M0 is ()
the carrier of M0 is set
bool the carrier of M0 is set
p is ext-real V34() real set
M is Element of the carrier of M0
{ b1 where b1 is Element of the carrier of M0 : not p <= (M0,M,b1) } is set
x is non empty ()
the carrier of x is non empty set
s is Element of the carrier of x
{ b1 where b1 is Element of the carrier of x : S1[b1] } is set
X is Element of bool the carrier of M0
r is Element of bool the carrier of M0
x is Element of bool the carrier of M0
s is Element of bool the carrier of M0
X is Element of bool the carrier of M0
X is Element of bool the carrier of M0
M0 is ()
the carrier of M0 is set
bool the carrier of M0 is set
M is Element of the carrier of M0
p is ext-real V34() real set
{ b1 where b1 is Element of the carrier of M0 : (M0,M,b1) <= p } is set
x is non empty ()
the carrier of x is non empty set
s is Element of the carrier of x
{ b1 where b1 is Element of the carrier of x : S1[b1] } is set
X is Element of bool the carrier of M0
r is Element of bool the carrier of M0
x is Element of bool the carrier of M0
s is Element of bool the carrier of M0
X is Element of bool the carrier of M0
X is Element of bool the carrier of M0
M0 is ()
the carrier of M0 is set
bool the carrier of M0 is set
M is Element of the carrier of M0
p is ext-real V34() real set
{ b1 where b1 is Element of the carrier of M0 : (M0,M,b1) = p } is set
x is non empty ()
the carrier of x is non empty set
s is Element of the carrier of x
{ b1 where b1 is Element of the carrier of x : S1[b1] } is set
X is Element of bool the carrier of M0
r is Element of bool the carrier of M0
x is Element of bool the carrier of M0
s is Element of bool the carrier of M0
X is Element of bool the carrier of M0
X is Element of bool the carrier of M0
M0 is ext-real V34() real set
M is ()
the carrier of M is set
r is Element of the carrier of M
p is Element of the carrier of M
(M,p,M0) is Element of bool the carrier of M
bool the carrier of M is set
(M,p,r) is ext-real V34() real Element of REAL
the of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like total V18([: the carrier of M, the carrier of M:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M, the carrier of M:],REAL:] is set
( the carrier of M, the carrier of M, the of M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M . [p,r] is ext-real V34() real set
x is non empty ()
the carrier of x is non empty set
s is Element of the carrier of x
{ b1 where b1 is Element of the carrier of x : not M0 <= (x,s,b1) } is set
X is Element of the carrier of M
(M,p,X) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,p,X) is ext-real V34() real Element of REAL
[p,X] is set
the of M . [p,X] is ext-real V34() real set
x is non empty ()
the carrier of x is non empty set
s is Element of the carrier of x
{ b1 where b1 is Element of the carrier of x : not M0 <= (x,s,b1) } is set
M0 is ext-real V34() real set
M is ()
the carrier of M is set
r is Element of the carrier of M
p is Element of the carrier of M
(M,p,M0) is Element of bool the carrier of M
bool the carrier of M is set
(M,p,r) is ext-real V34() real Element of REAL
the of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like total V18([: the carrier of M, the carrier of M:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M, the carrier of M:],REAL:] is set
( the carrier of M, the carrier of M, the of M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M . [p,r] is ext-real V34() real set
x is non empty ()
the carrier of x is non empty set
s is Element of the carrier of x
{ b1 where b1 is Element of the carrier of x : (x,s,b1) <= M0 } is set
X is Element of the carrier of M
(M,p,X) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,p,X) is ext-real V34() real Element of REAL
[p,X] is set
the of M . [p,X] is ext-real V34() real set
x is non empty ()
the carrier of x is non empty set
s is Element of the carrier of x
{ b1 where b1 is Element of the carrier of x : (x,s,b1) <= M0 } is set
M0 is ext-real V34() real set
M is ()
the carrier of M is set
r is Element of the carrier of M
p is Element of the carrier of M
(M,p,M0) is Element of bool the carrier of M
bool the carrier of M is set
(M,p,r) is ext-real V34() real Element of REAL
the of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like total V18([: the carrier of M, the carrier of M:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M, the carrier of M:],REAL:] is set
( the carrier of M, the carrier of M, the of M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M . [p,r] is ext-real V34() real set
x is non empty ()
the carrier of x is non empty set
s is Element of the carrier of x
{ b1 where b1 is Element of the carrier of x : (x,s,b1) = M0 } is set
X is Element of the carrier of M
(M,p,X) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,p,X) is ext-real V34() real Element of REAL
[p,X] is set
the of M . [p,X] is ext-real V34() real set
x is non empty ()
the carrier of x is non empty set
s is Element of the carrier of x
{ b1 where b1 is Element of the carrier of x : (x,s,b1) = M0 } is set
M0 is ext-real V34() real set
M is ()
the carrier of M is set
p is Element of the carrier of M
(M,p,M0) is Element of bool the carrier of M
bool the carrier of M is set
(M,p,M0) is Element of bool the carrier of M
r is Element of the carrier of M
(M,p,r) is ext-real V34() real Element of REAL
the of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like total V18([: the carrier of M, the carrier of M:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M, the carrier of M:],REAL:] is set
( the carrier of M, the carrier of M, the of M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M . [p,r] is ext-real V34() real set
{ b1 where b1 is Element of the carrier of M : (M,p,b1) <= M0 } is set
M0 is ext-real V34() real set
M is ()
the carrier of M is set
p is Element of the carrier of M
(M,p,M0) is Element of bool the carrier of M
bool the carrier of M is set
(M,p,M0) is Element of bool the carrier of M
r is Element of the carrier of M
(M,p,r) is ext-real V34() real Element of REAL
the of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like total V18([: the carrier of M, the carrier of M:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M, the carrier of M:],REAL:] is set
( the carrier of M, the carrier of M, the of M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M . [p,r] is ext-real V34() real set
{ b1 where b1 is Element of the carrier of M : (M,p,b1) <= M0 } is set
M0 is ext-real V34() real set
M is ()
the carrier of M is set
p is Element of the carrier of M
(M,p,M0) is Element of bool the carrier of M
bool the carrier of M is set
(M,p,M0) is Element of bool the carrier of M
(M,p,M0) \/ (M,p,M0) is Element of bool the carrier of M
(M,p,M0) is Element of bool the carrier of M
r is Element of the carrier of M
(M,p,r) is ext-real V34() real Element of REAL
the of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like total V18([: the carrier of M, the carrier of M:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M, the carrier of M:],REAL:] is set
( the carrier of M, the carrier of M, the of M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M . [p,r] is ext-real V34() real set
M is non empty ()
the carrier of M is non empty set
p is Element of the carrier of M
M0 is ext-real V34() real set
(M,p,M0) is Element of bool the carrier of M
bool the carrier of M is set
{ b1 where b1 is Element of the carrier of M : not M0 <= (M,p,b1) } is set
M is non empty ()
the carrier of M is non empty set
p is Element of the carrier of M
M0 is ext-real V34() real set
(M,p,M0) is Element of bool the carrier of M
bool the carrier of M is set
{ b1 where b1 is Element of the carrier of M : (M,p,b1) <= M0 } is set
M is non empty ()
the carrier of M is non empty set
p is Element of the carrier of M
M0 is ext-real V34() real set
(M,p,M0) is Element of bool the carrier of M
bool the carrier of M is set
{ b1 where b1 is Element of the carrier of M : (M,p,b1) = M0 } is set

M0 is set
() . (M0,M0) is ext-real natural V34() real set
[M0,M0] is set
() . [M0,M0] is ext-real natural V34() real V60() set
dom () is Relation-like set
M0 is ext-real natural V34() real V59() V60() Element of 1
M is ext-real natural V34() real V59() V60() Element of 1
(1,1,(),M0,M) is ext-real natural V34() real Element of REAL
[M0,M] is set
() . [M0,M] is ext-real natural V34() real V60() set
M0 is ext-real natural V34() real V59() V60() Element of 1
M is ext-real natural V34() real V59() V60() Element of 1
(1,1,(),M0,M) is ext-real natural V34() real Element of REAL
[M0,M] is set
() . [M0,M] is ext-real natural V34() real V60() set
(1,1,(),M,M0) is ext-real natural V34() real Element of REAL
[M,M0] is set
() . [M,M0] is ext-real natural V34() real V60() set
M0 is ext-real natural V34() real V59() V60() Element of 1
p is ext-real natural V34() real V59() V60() Element of 1
(1,1,(),M0,p) is ext-real natural V34() real Element of REAL
[M0,p] is set
() . [M0,p] is ext-real natural V34() real V60() set
M is ext-real natural V34() real V59() V60() Element of 1
(1,1,(),M0,M) is ext-real natural V34() real Element of REAL
[M0,M] is set
() . [M0,M] is ext-real natural V34() real V60() set
(1,1,(),M,p) is ext-real natural V34() real Element of REAL
[M,p] is set
() . [M,p] is ext-real natural V34() real V60() set
(1,1,(),M0,M) + (1,1,(),M,p) is ext-real V34() real Element of REAL
M0 is ext-real natural V34() real V59() V60() Element of 1
p is ext-real natural V34() real V59() V60() Element of 1
(1,1,(),M0,p) is ext-real natural V34() real Element of REAL
[M0,p] is set
() . [M0,p] is ext-real natural V34() real V60() set
M is ext-real natural V34() real V59() V60() Element of 1
(1,1,(),M0,M) is ext-real natural V34() real Element of REAL
[M0,M] is set
() . [M0,M] is ext-real natural V34() real V60() set
(1,1,(),M,p) is ext-real natural V34() real Element of REAL
[M,p] is set
() . [M,p] is ext-real natural V34() real V60() set
max ((1,1,(),M0,M),(1,1,(),M,p)) is ext-real V34() real set
(1,()) is () ()
M is non empty set
[:M,M:] is Relation-like set

bool [:[:M,M:],REAL:] is set
M is non empty ()
the carrier of M is non empty set
the of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like total V18([: the carrier of M, the carrier of M:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M, the carrier of M:],REAL:] is set
p is Element of the carrier of M
r is Element of the carrier of M
( the carrier of M, the carrier of M, the of M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M . [p,r] is ext-real V34() real set
(M,p,r) is ext-real V34() real Element of REAL
p is Element of the carrier of M
r is Element of the carrier of M
(M,p,r) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M . [p,r] is ext-real V34() real set
the carrier of (1,()) is non empty set
M is Element of the carrier of (1,())
((1,()),M,M) is ext-real V34() real Element of REAL
the of (1,()) is Relation-like [: the carrier of (1,()), the carrier of (1,()):] -defined REAL -valued Function-like total V18([: the carrier of (1,()), the carrier of (1,()):], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of (1,()), the carrier of (1,()):],REAL:]
[: the carrier of (1,()), the carrier of (1,()):] is Relation-like set
[:[: the carrier of (1,()), the carrier of (1,()):],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of (1,()), the carrier of (1,()):],REAL:] is set
( the carrier of (1,()), the carrier of (1,()), the of (1,()),M,M) is ext-real V34() real Element of REAL
[M,M] is set
the of (1,()) . [M,M] is ext-real V34() real set
M is Element of the carrier of (1,())
p is Element of the carrier of (1,())
((1,()),M,p) is ext-real V34() real Element of REAL
the of (1,()) is Relation-like [: the carrier of (1,()), the carrier of (1,()):] -defined REAL -valued Function-like total V18([: the carrier of (1,()), the carrier of (1,()):], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of (1,()), the carrier of (1,()):],REAL:]
[: the carrier of (1,()), the carrier of (1,()):] is Relation-like set
[:[: the carrier of (1,()), the carrier of (1,()):],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of (1,()), the carrier of (1,()):],REAL:] is set
( the carrier of (1,()), the carrier of (1,()), the of (1,()),M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of (1,()) . [M,p] is ext-real V34() real set
((1,()),p,M) is ext-real V34() real Element of REAL
( the carrier of (1,()), the carrier of (1,()), the of (1,()),p,M) is ext-real V34() real Element of REAL
[p,M] is set
the of (1,()) . [p,M] is ext-real V34() real set
M is Element of the carrier of (1,())
p is Element of the carrier of (1,())
((1,()),M,p) is ext-real V34() real Element of REAL
the of (1,()) is Relation-like [: the carrier of (1,()), the carrier of (1,()):] -defined REAL -valued Function-like total V18([: the carrier of (1,()), the carrier of (1,()):], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of (1,()), the carrier of (1,()):],REAL:]
[: the carrier of (1,()), the carrier of (1,()):] is Relation-like set
[:[: the carrier of (1,()), the carrier of (1,()):],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of (1,()), the carrier of (1,()):],REAL:] is set
( the carrier of (1,()), the carrier of (1,()), the of (1,()),M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of (1,()) . [M,p] is ext-real V34() real set
M is Element of the carrier of (1,())
r is Element of the carrier of (1,())
((1,()),M,r) is ext-real V34() real Element of REAL
the of (1,()) is Relation-like [: the carrier of (1,()), the carrier of (1,()):] -defined REAL -valued Function-like total V18([: the carrier of (1,()), the carrier of (1,()):], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of (1,()), the carrier of (1,()):],REAL:]
[: the carrier of (1,()), the carrier of (1,()):] is Relation-like set
[:[: the carrier of (1,()), the carrier of (1,()):],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of (1,()), the carrier of (1,()):],REAL:] is set
( the carrier of (1,()), the carrier of (1,()), the of (1,()),M,r) is ext-real V34() real Element of REAL
[M,r] is set
the of (1,()) . [M,r] is ext-real V34() real set
p is Element of the carrier of (1,())
((1,()),M,p) is ext-real V34() real Element of REAL
( the carrier of (1,()), the carrier of (1,()), the of (1,()),M,p) is ext-real V34() real Element of REAL
[M,p] is set
the of (1,()) . [M,p] is ext-real V34() real set
((1,()),p,r) is ext-real V34() real Element of REAL
( the carrier of (1,()), the carrier of (1,()), the of (1,()),p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of (1,()) . [p,r] is ext-real V34() real set
((1,()),M,p) + ((1,()),p,r) is ext-real V34() real Element of REAL
M is non empty () () () () () ()
the carrier of M is non empty set
p is Element of the carrier of M
x is Element of the carrier of M
(M,p,x) is ext-real V34() real Element of REAL
the of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like total V18([: the carrier of M, the carrier of M:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M, the carrier of M:],REAL:] is set
( the carrier of M, the carrier of M, the of M,p,x) is ext-real V34() real Element of REAL
[p,x] is set
the of M . [p,x] is ext-real V34() real set
r is Element of the carrier of M
(M,p,r) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M . [p,r] is ext-real V34() real set
(M,r,x) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,r,x) is ext-real V34() real Element of REAL
[r,x] is set
the of M . [r,x] is ext-real V34() real set
max ((M,p,r),(M,r,x)) is ext-real V34() real set
M is non empty () () ()
the carrier of M is non empty set
p is Element of the carrier of M
r is Element of the carrier of M
(M,p,r) is ext-real V34() real Element of REAL
the of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like total V18([: the carrier of M, the carrier of M:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M, the carrier of M:],REAL:] is set
( the carrier of M, the carrier of M, the of M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M . [p,r] is ext-real V34() real set
M is non empty () () () () ()
the carrier of M is non empty set
p is Element of the carrier of M
r is Element of the carrier of M
(M,p,r) is ext-real V34() real Element of REAL
the of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like total V18([: the carrier of M, the carrier of M:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M, the carrier of M:],REAL:] is set
( the carrier of M, the carrier of M, the of M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M . [p,r] is ext-real V34() real set
M is non empty () () () () ()
the carrier of M is non empty set
p is Element of the carrier of M
r is Element of the carrier of M
(M,p,r) is ext-real V34() real Element of REAL
the of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like total V18([: the carrier of M, the carrier of M:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M, the carrier of M:],REAL:] is set
( the carrier of M, the carrier of M, the of M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M . [p,r] is ext-real V34() real set
(M,r,p) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,r,p) is ext-real V34() real Element of REAL
[r,p] is set
the of M . [r,p] is ext-real V34() real set
x is Element of the carrier of M
(M,r,x) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,r,x) is ext-real V34() real Element of REAL
[r,x] is set
the of M . [r,x] is ext-real V34() real set
max ((M,p,r),(M,r,x)) is ext-real V34() real set
(M,p,r) + (M,r,x) is ext-real V34() real Element of REAL
(M,p,x) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,p,x) is ext-real V34() real Element of REAL
[p,x] is set
the of M . [p,x] is ext-real V34() real set
2 is non empty ext-real positive natural V34() real V59() V60() V71() V72() V73() V74() V75() V76() Element of NAT

bool [:[:2,2:],REAL:] is set

M is ext-real natural V34() real V59() V60() Element of 2
p is ext-real natural V34() real V59() V60() Element of 2
(2,2,(),M,p) is ext-real V34() real Element of REAL
[M,p] is set
() . [M,p] is ext-real V34() real set
M is ext-real natural V34() real V59() V60() Element of 2
p is ext-real natural V34() real V59() V60() Element of 2
(2,2,(),M,p) is ext-real V34() real Element of REAL
[M,p] is set
() . [M,p] is ext-real V34() real set
(2,2,(),p,M) is ext-real V34() real Element of REAL
[p,M] is set
() . [p,M] is ext-real V34() real set
M is ext-real natural V34() real V59() V60() Element of 2
r is ext-real natural V34() real V59() V60() Element of 2
(2,2,(),M,r) is ext-real V34() real Element of REAL
[M,r] is set
() . [M,r] is ext-real V34() real set
p is ext-real natural V34() real V59() V60() Element of 2
(2,2,(),M,p) is ext-real V34() real Element of REAL
[M,p] is set
() . [M,p] is ext-real V34() real set
(2,2,(),p,r) is ext-real V34() real Element of REAL
[p,r] is set
() . [p,r] is ext-real V34() real set
(2,2,(),M,p) + (2,2,(),p,r) is ext-real V34() real Element of REAL
(2,()) is () ()
() is ()
the carrier of (2,()) is set
p is Element of the carrier of (2,())
r is Element of the carrier of (2,())
((2,()),p,r) is ext-real V34() real Element of REAL
the of (2,()) is Relation-like [: the carrier of (2,()), the carrier of (2,()):] -defined REAL -valued Function-like total V18([: the carrier of (2,()), the carrier of (2,()):], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of (2,()), the carrier of (2,()):],REAL:]
[: the carrier of (2,()), the carrier of (2,()):] is Relation-like set
[:[: the carrier of (2,()), the carrier of (2,()):],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of (2,()), the carrier of (2,()):],REAL:] is set
( the carrier of (2,()), the carrier of (2,()), the of (2,()),p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of (2,()) . [p,r] is ext-real V34() real set
((2,()),r,p) is ext-real V34() real Element of REAL
( the carrier of (2,()), the carrier of (2,()), the of (2,()),r,p) is ext-real V34() real Element of REAL
[r,p] is set
the of (2,()) . [r,p] is ext-real V34() real set
x is Element of the carrier of (2,())
X is Element of the carrier of (2,())
((2,()),x,X) is ext-real V34() real Element of REAL
( the carrier of (2,()), the carrier of (2,()), the of (2,()),x,X) is ext-real V34() real Element of REAL
[x,X] is set
the of (2,()) . [x,X] is ext-real V34() real set
s is Element of the carrier of (2,())
((2,()),x,s) is ext-real V34() real Element of REAL
( the carrier of (2,()), the carrier of (2,()), the of (2,()),x,s) is ext-real V34() real Element of REAL
[x,s] is set
the of (2,()) . [x,s] is ext-real V34() real set
((2,()),s,X) is ext-real V34() real Element of REAL
( the carrier of (2,()), the carrier of (2,()), the of (2,()),s,X) is ext-real V34() real Element of REAL
[s,X] is set
the of (2,()) . [s,X] is ext-real V34() real set
((2,()),x,s) + ((2,()),s,X) is ext-real V34() real Element of REAL
p is Element of the carrier of (2,())
((2,()),p,p) is ext-real V34() real Element of REAL
the of (2,()) is Relation-like [: the carrier of (2,()), the carrier of (2,()):] -defined REAL -valued Function-like total V18([: the carrier of (2,()), the carrier of (2,()):], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of (2,()), the carrier of (2,()):],REAL:]
[: the carrier of (2,()), the carrier of (2,()):] is Relation-like set
[:[: the carrier of (2,()), the carrier of (2,()):],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of (2,()), the carrier of (2,()):],REAL:] is set
( the carrier of (2,()), the carrier of (2,()), the of (2,()),p,p) is ext-real V34() real Element of REAL
[p,p] is set
the of (2,()) . [p,p] is ext-real V34() real set
M is ()
the carrier of M is set
M is non empty () () () ()
the carrier of M is non empty set
p is Element of the carrier of M
r is Element of the carrier of M
x is Element of the carrier of M
(M,x,p) is ext-real V34() real Element of REAL
the of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like total V18([: the carrier of M, the carrier of M:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M, the carrier of M:],REAL:] is set
( the carrier of M, the carrier of M, the of M,x,p) is ext-real V34() real Element of REAL
[x,p] is set
the of M . [x,p] is ext-real V34() real set
(M,x,r) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,x,r) is ext-real V34() real Element of REAL
[x,r] is set
the of M . [x,r] is ext-real V34() real set
(M,r,p) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,r,p) is ext-real V34() real Element of REAL
[r,p] is set
the of M . [r,p] is ext-real V34() real set
(M,x,r) + (M,r,p) is ext-real V34() real Element of REAL
(M,p,x) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,p,x) is ext-real V34() real Element of REAL
[p,x] is set
the of M . [p,x] is ext-real V34() real set
(M,p,r) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M . [p,r] is ext-real V34() real set
(M,r,x) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,r,x) is ext-real V34() real Element of REAL
[r,x] is set
the of M . [r,x] is ext-real V34() real set
(M,p,r) + (M,r,x) is ext-real V34() real Element of REAL
M is () () () () ()
the carrier of M is set
p is Element of the carrier of M
r is Element of the carrier of M
x is Element of the carrier of M
(M,p,x) is ext-real V34() real Element of REAL
the of M is Relation-like [: the carrier of M, the carrier of M:] -defined REAL -valued Function-like total V18([: the carrier of M, the carrier of M:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of M, the carrier of M:],REAL:]
[: the carrier of M, the carrier of M:] is Relation-like set
[:[: the carrier of M, the carrier of M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:[: the carrier of M, the carrier of M:],REAL:] is set
( the carrier of M, the carrier of M, the of M,p,x) is ext-real V34() real Element of REAL
[p,x] is set
the of M . [p,x] is ext-real V34() real set
(M,p,r) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,p,r) is ext-real V34() real Element of REAL
[p,r] is set
the of M . [p,r] is ext-real V34() real set
(M,r,x) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,r,x) is ext-real V34() real Element of