:: 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

bool REAL is set

{} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() set

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

the Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() set is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() 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

bool omega is set

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

[:1,1:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:1,1:] is set

[:[:1,1:],1:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

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

0 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty ext-real natural V34() real V59() V60() complex-valued ext-real-valued real-valued natural-valued V71() V72() V73() V74() V75() V76() V77() Element of NAT

{{}} is functional non empty 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

[:[:M0,M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set

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

p is Relation-like [:M0,M:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[:M0,M:],REAL:]

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

dom p is Relation-like set

dom p is Relation-like set

dom p is Relation-like 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

({},{}) :-> {} is Relation-like [:{{}},{{}}:] -defined {{}} -valued Function-like total V18([:{{}},{{}}:],{{}}) Element of bool [:[:{{}},{{}}:],{{}}:]

[:{{}},{{}}:] is Relation-like set

[:[:{{}},{{}}:],{{}}:] is Relation-like set

bool [:[:{{}},{{}}:],{{}}:] is set

[:[:1,1:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set

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

op2 is Relation-like [:1,1:] -defined 1 -valued Function-like total V18([:1,1:],1) complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:1,1:],1:]

op2 is Relation-like [:1,1:] -defined 1 -valued Function-like total V18([:1,1:],1) complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:1,1:],1:]

op2 . ({},{}) is set

[{},{}] is set

op2 . [{},{}] 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

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

M0 is Relation-like Function-like set

M0 is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued 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

[:[:M0,M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set

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

() is Relation-like [:1,1:] -defined REAL -valued RAT -valued Function-like total V18([:1,1:], REAL ) complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:1,1:],REAL:]

(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

[:[:M0,M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set

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

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

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

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

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:]

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

p is Relation-like [:M0,M0:] -defined REAL -valued Function-like total V18([:M0,M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:M0,M0:],REAL:]

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) is Relation-like [:M0,M0:] -defined REAL -valued Function-like total V18([:M0,M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:M0,M0:],REAL:]

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

[:[:M0,M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set

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

(M0,(M0)) is () ()

M0 is non empty set

(M0) is () ()

(M0) is Relation-like [:M0,M0:] -defined REAL -valued Function-like total V18([:M0,M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:M0,M0:],REAL:]

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

[:[:M0,M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set

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

(M0,(M0)) is () ()

M0 is set

(M0) is () ()

(M0) is Relation-like [:M0,M0:] -defined REAL -valued Function-like total V18([:M0,M0:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:M0,M0:],REAL:]

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

[:[:M0,M0:],REAL:] is Relation-like complex-valued ext-real-valued real-valued 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

[:REAL,REAL:] is Relation-like complex-valued ext-real-valued real-valued set

[:[:REAL,REAL:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set

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

M0 is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

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

M0 is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]

M is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],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

() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V18([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],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

c

(M0,X,c

( the carrier of M0, the carrier of M0, the of M0,X,c

[X,c

the of M0 . [X,c

c

(M0,X,c

( the carrier of M0, the carrier of M0, the of M0,X,c

[X,c

the of M0 . [X,c

(M0,c

( the carrier of M0, the carrier of M0, the of M0,c

[c

the of M0 . [c

(M0,X,c

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

{ b

x is non empty ()

the carrier of x is non empty set

s is Element of the carrier of x

{ b

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

{ b

x is non empty ()

the carrier of x is non empty set

s is Element of the carrier of x

{ b

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

{ b

x is non empty ()

the carrier of x is non empty set

s is Element of the carrier of x

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

() is Relation-like [:1,1:] -defined REAL -valued RAT -valued Function-like total V18([:1,1:], REAL ) complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:1,1:],REAL:]

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

[:[:M,M:],REAL:] is Relation-like complex-valued ext-real-valued real-valued 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

[:2,2:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

[:2,2:] --> 0 is Relation-like [:2,2:] -defined REAL -valued RAT -valued INT -valued Function-like total V18([:2,2:], REAL ) complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:2,2:],REAL:]

[:[:2,2:],REAL:] is Relation-like complex-valued ext-real-valued real-valued set

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

() is Relation-like [:2,2:] -defined REAL -valued Function-like total V18([:2,2:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:2,2:],REAL:]

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