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
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
() 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 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,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,r,p) + (M,p,x) is ext-real V34() real Element of REAL
(M,p,r) + ((M,r,p) + (M,p,x)) is ext-real V34() real Element of REAL
(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,p,r) + (M,r,x)) + (M,x,r) 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
s 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 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,p,s) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,p,s) is ext-real V34() real Element of REAL
[p,s] is set
the of M . [p,s] is ext-real V34() real set
(M,x,s) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,x,s) is ext-real V34() real Element of REAL
[x,s] is set
the of M . [x,s] is ext-real V34() real set
((M,p,r) + (M,r,x)) + (M,x,s) is ext-real V34() real Element of REAL
(M,r,s) is ext-real V34() real Element of REAL
( the carrier of M, the carrier of M, the of M,r,s) is ext-real V34() real Element of REAL
[r,s] is set
the of M . [r,s] is ext-real V34() real set
(M,p,r) + (M,r,s) is ext-real V34() real Element of REAL
(M,r,x) + (M,x,s) is ext-real V34() real Element of REAL
((M,r,x) + (M,x,s)) + (M,p,r) is ext-real V34() real Element of REAL
(M,p,r) + ((M,r,x) + (M,x,s)) 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
r is Element of the carrier of M
{ b1 where b1 is Element of the carrier of M : (M,p,b1,r) } is set
bool the carrier of M is set
{ b1 where b1 is Element of the carrier of M : S1[b1] } is set
M is non empty () () () () () ()
the carrier of M is non empty set
x is Element of the carrier of M
p is Element of the carrier of M
r is Element of the carrier of M
(M,p,r) 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,r) } is set
s is Element of the carrier of M
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
{ b1 where b1 is Element of the carrier of M : (M,p,b1,r) } is set
{p,r} is non empty set
{ b1 where b1 is Element of the carrier of M : (M,p,b1,r) } \/ {p,r} is non empty set
bool the carrier of M is set
{ b1 where b1 is Element of the carrier of M : S1[b1] } is set
M is non empty ()
the carrier of M is non empty set
x is Element of the carrier of M
p is Element of the carrier of M
r is Element of the carrier of M
(M,p,r) 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,r) } is set
{p,r} is non empty set
{ b1 where b1 is Element of the carrier of M : (M,p,b1,r) } \/ {p,r} is non empty set
s is Element of the carrier of M