NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V138() Element of K6(REAL)
REAL is non empty V33() complex-membered ext-real-membered real-membered V138() set
K6(REAL) is set
COMPLEX is non empty V33() complex-membered V138() set
NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V138() set
K6(NAT) is set
K6(NAT) is set
1 is non empty set
{} is empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V138() set
K7(REAL,REAL) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
A is Relation-like K7(REAL,REAL) -defined REAL -valued V21() quasi_total Element of K6(K7(K7(REAL,REAL),REAL))
A is Relation-like K7(REAL,REAL) -defined REAL -valued V21() quasi_total Element of K6(K7(K7(REAL,REAL),REAL))
q is Relation-like K7(REAL,REAL) -defined REAL -valued V21() quasi_total Element of K6(K7(K7(REAL,REAL),REAL))
p is V11() ext-real V15() Element of REAL
r is V11() ext-real V15() Element of REAL
A . (p,r) is V11() ext-real V15() Element of REAL
q . (p,r) is V11() ext-real V15() Element of REAL
min (p,r) is V11() ext-real V15() Element of REAL
A is Relation-like K7(REAL,REAL) -defined REAL -valued V21() quasi_total Element of K6(K7(K7(REAL,REAL),REAL))
A is Relation-like K7(REAL,REAL) -defined REAL -valued V21() quasi_total Element of K6(K7(K7(REAL,REAL),REAL))
q is Relation-like K7(REAL,REAL) -defined REAL -valued V21() quasi_total Element of K6(K7(K7(REAL,REAL),REAL))
p is V11() ext-real V15() Element of REAL
r is V11() ext-real V15() Element of REAL
A . (p,r) is V11() ext-real V15() Element of REAL
q . (p,r) is V11() ext-real V15() Element of REAL
max (p,r) is V11() ext-real V15() Element of REAL
() is Relation-like K7(REAL,REAL) -defined REAL -valued V21() quasi_total Element of K6(K7(K7(REAL,REAL),REAL))
() is Relation-like K7(REAL,REAL) -defined REAL -valued V21() quasi_total Element of K6(K7(K7(REAL,REAL),REAL))
LattStr(# REAL,(),() #) is non empty strict LattStr
() is strict LattStr
the carrier of () is set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
A "\/" q is V11() ext-real V15() Element of the carrier of ()
the L_join of () is Relation-like K7( the carrier of (), the carrier of ()) -defined the carrier of () -valued V21() quasi_total Element of K6(K7(K7( the carrier of (), the carrier of ()), the carrier of ()))
K7( the carrier of (), the carrier of ()) is set
K7(K7( the carrier of (), the carrier of ()), the carrier of ()) is set
K6(K7(K7( the carrier of (), the carrier of ()), the carrier of ())) is set
the L_join of () . (A,q) is V11() ext-real V15() Element of the carrier of ()
max (A,q) is V11() ext-real V15() set
A "/\" q is V11() ext-real V15() Element of the carrier of ()
the L_meet of () is Relation-like K7( the carrier of (), the carrier of ()) -defined the carrier of () -valued V21() quasi_total Element of K6(K7(K7( the carrier of (), the carrier of ()), the carrier of ()))
the L_meet of () . (A,q) is V11() ext-real V15() Element of the carrier of ()
min (A,q) is V11() ext-real V15() set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
A "\/" q is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (A,q) is V11() ext-real V15() Element of the carrier of ()
max (A,q) is V11() ext-real V15() set
q "\/" A is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (q,A) is V11() ext-real V15() Element of the carrier of ()
max (q,A) is V11() ext-real V15() set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
p is V11() ext-real V15() Element of the carrier of ()
q "\/" p is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (q,p) is V11() ext-real V15() Element of the carrier of ()
max (q,p) is V11() ext-real V15() set
A "\/" (q "\/" p) is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (A,(q "\/" p)) is V11() ext-real V15() Element of the carrier of ()
max (A,(q "\/" p)) is V11() ext-real V15() set
A "\/" q is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (A,q) is V11() ext-real V15() Element of the carrier of ()
max (A,q) is V11() ext-real V15() set
(A "\/" q) "\/" p is V11() ext-real V15() Element of the carrier of ()
the L_join of () . ((A "\/" q),p) is V11() ext-real V15() Element of the carrier of ()
max ((A "\/" q),p) is V11() ext-real V15() set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
A "/\" q is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,q) is V11() ext-real V15() Element of the carrier of ()
min (A,q) is V11() ext-real V15() set
(A "/\" q) "\/" q is V11() ext-real V15() Element of the carrier of ()
the L_join of () . ((A "/\" q),q) is V11() ext-real V15() Element of the carrier of ()
max ((A "/\" q),q) is V11() ext-real V15() set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
A "/\" q is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,q) is V11() ext-real V15() Element of the carrier of ()
min (A,q) is V11() ext-real V15() set
q "/\" A is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (q,A) is V11() ext-real V15() Element of the carrier of ()
min (q,A) is V11() ext-real V15() set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
p is V11() ext-real V15() Element of the carrier of ()
q "/\" p is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (q,p) is V11() ext-real V15() Element of the carrier of ()
min (q,p) is V11() ext-real V15() set
A "/\" (q "/\" p) is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,(q "/\" p)) is V11() ext-real V15() Element of the carrier of ()
min (A,(q "/\" p)) is V11() ext-real V15() set
A "/\" q is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,q) is V11() ext-real V15() Element of the carrier of ()
min (A,q) is V11() ext-real V15() set
(A "/\" q) "/\" p is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . ((A "/\" q),p) is V11() ext-real V15() Element of the carrier of ()
min ((A "/\" q),p) is V11() ext-real V15() set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
A "\/" q is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (A,q) is V11() ext-real V15() Element of the carrier of ()
max (A,q) is V11() ext-real V15() set
A "/\" (A "\/" q) is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,(A "\/" q)) is V11() ext-real V15() Element of the carrier of ()
min (A,(A "\/" q)) is V11() ext-real V15() set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
p is V11() ext-real V15() Element of the carrier of ()
q "\/" p is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (q,p) is V11() ext-real V15() Element of the carrier of ()
max (q,p) is V11() ext-real V15() set
A "/\" (q "\/" p) is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,(q "\/" p)) is V11() ext-real V15() Element of the carrier of ()
min (A,(q "\/" p)) is V11() ext-real V15() set
A "/\" q is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,q) is V11() ext-real V15() Element of the carrier of ()
min (A,q) is V11() ext-real V15() set
A "/\" p is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,p) is V11() ext-real V15() Element of the carrier of ()
min (A,p) is V11() ext-real V15() set
(A "/\" q) "\/" (A "/\" p) is V11() ext-real V15() Element of the carrier of ()
the L_join of () . ((A "/\" q),(A "/\" p)) is V11() ext-real V15() Element of the carrier of ()
max ((A "/\" q),(A "/\" p)) is V11() ext-real V15() set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
() . (A,q) is set
() . (q,A) is set
q "\/" A is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (q,A) is V11() ext-real V15() Element of the carrier of ()
max (q,A) is V11() ext-real V15() set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
() . (A,q) is set
() . (q,A) is set
q "/\" A is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (q,A) is V11() ext-real V15() Element of the carrier of ()
min (q,A) is V11() ext-real V15() set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
() . (A,q) is set
() . (q,A) is set
p is V11() ext-real V15() Element of the carrier of ()
() . (q,p) is set
() . (A,(() . (q,p))) is set
() . ((() . (q,p)),A) is set
() . ((() . (A,q)),p) is set
() . ((() . (q,A)),p) is set
() . (p,A) is set
() . ((() . (p,A)),q) is set
() . (p,q) is set
() . ((() . (p,q)),A) is set
() . (A,p) is set
() . ((() . (A,p)),q) is set
q "\/" p is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (q,p) is V11() ext-real V15() Element of the carrier of ()
max (q,p) is V11() ext-real V15() set
(q "\/" p) "\/" A is V11() ext-real V15() Element of the carrier of ()
the L_join of () . ((q "\/" p),A) is V11() ext-real V15() Element of the carrier of ()
max ((q "\/" p),A) is V11() ext-real V15() set
A "\/" (q "\/" p) is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (A,(q "\/" p)) is V11() ext-real V15() Element of the carrier of ()
max (A,(q "\/" p)) is V11() ext-real V15() set
A "\/" q is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (A,q) is V11() ext-real V15() Element of the carrier of ()
max (A,q) is V11() ext-real V15() set
(A "\/" q) "\/" p is V11() ext-real V15() Element of the carrier of ()
the L_join of () . ((A "\/" q),p) is V11() ext-real V15() Element of the carrier of ()
max ((A "\/" q),p) is V11() ext-real V15() set
q "\/" A is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (q,A) is V11() ext-real V15() Element of the carrier of ()
max (q,A) is V11() ext-real V15() set
(q "\/" A) "\/" p is V11() ext-real V15() Element of the carrier of ()
the L_join of () . ((q "\/" A),p) is V11() ext-real V15() Element of the carrier of ()
max ((q "\/" A),p) is V11() ext-real V15() set
p "\/" A is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (p,A) is V11() ext-real V15() Element of the carrier of ()
max (p,A) is V11() ext-real V15() set
(p "\/" A) "\/" q is V11() ext-real V15() Element of the carrier of ()
the L_join of () . ((p "\/" A),q) is V11() ext-real V15() Element of the carrier of ()
max ((p "\/" A),q) is V11() ext-real V15() set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
() . (A,q) is set
() . (q,A) is set
p is V11() ext-real V15() Element of the carrier of ()
() . (q,p) is set
() . (A,(() . (q,p))) is set
() . ((() . (q,p)),A) is set
() . ((() . (A,q)),p) is set
() . ((() . (q,A)),p) is set
() . (p,A) is set
() . ((() . (p,A)),q) is set
() . (p,q) is set
() . ((() . (p,q)),A) is set
() . (A,p) is set
() . ((() . (A,p)),q) is set
q "/\" p is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (q,p) is V11() ext-real V15() Element of the carrier of ()
min (q,p) is V11() ext-real V15() set
(q "/\" p) "/\" A is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . ((q "/\" p),A) is V11() ext-real V15() Element of the carrier of ()
min ((q "/\" p),A) is V11() ext-real V15() set
A "/\" (q "/\" p) is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,(q "/\" p)) is V11() ext-real V15() Element of the carrier of ()
min (A,(q "/\" p)) is V11() ext-real V15() set
A "/\" q is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,q) is V11() ext-real V15() Element of the carrier of ()
min (A,q) is V11() ext-real V15() set
(A "/\" q) "/\" p is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . ((A "/\" q),p) is V11() ext-real V15() Element of the carrier of ()
min ((A "/\" q),p) is V11() ext-real V15() set
q "/\" A is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (q,A) is V11() ext-real V15() Element of the carrier of ()
min (q,A) is V11() ext-real V15() set
(q "/\" A) "/\" p is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . ((q "/\" A),p) is V11() ext-real V15() Element of the carrier of ()
min ((q "/\" A),p) is V11() ext-real V15() set
p "/\" A is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (p,A) is V11() ext-real V15() Element of the carrier of ()
min (p,A) is V11() ext-real V15() set
(p "/\" A) "/\" q is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . ((p "/\" A),q) is V11() ext-real V15() Element of the carrier of ()
min ((p "/\" A),q) is V11() ext-real V15() set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
() . (A,q) is set
() . ((() . (A,q)),q) is set
() . (q,(() . (A,q))) is set
() . (q,A) is set
() . (q,(() . (q,A))) is set
() . ((() . (q,A)),q) is set
A "/\" q is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,q) is V11() ext-real V15() Element of the carrier of ()
min (A,q) is V11() ext-real V15() set
(A "/\" q) "\/" q is V11() ext-real V15() Element of the carrier of ()
the L_join of () . ((A "/\" q),q) is V11() ext-real V15() Element of the carrier of ()
max ((A "/\" q),q) is V11() ext-real V15() set
q "/\" A is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (q,A) is V11() ext-real V15() Element of the carrier of ()
min (q,A) is V11() ext-real V15() set
() . (q,(q "/\" A)) is set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
() . (A,q) is set
() . (A,(() . (A,q))) is set
() . (q,A) is set
() . ((() . (q,A)),A) is set
() . (A,(() . (q,A))) is set
() . ((() . (A,q)),A) is set
A "\/" q is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (A,q) is V11() ext-real V15() Element of the carrier of ()
max (A,q) is V11() ext-real V15() set
A "/\" (A "\/" q) is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,(A "\/" q)) is V11() ext-real V15() Element of the carrier of ()
min (A,(A "\/" q)) is V11() ext-real V15() set
q "\/" A is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (q,A) is V11() ext-real V15() Element of the carrier of ()
max (q,A) is V11() ext-real V15() set
() . ((q "\/" A),A) is set
A is V11() ext-real V15() Element of the carrier of ()
q is V11() ext-real V15() Element of the carrier of ()
() . (A,q) is set
p is V11() ext-real V15() Element of the carrier of ()
() . (q,p) is set
() . (A,(() . (q,p))) is set
() . (A,p) is set
() . ((() . (A,q)),(() . (A,p))) is set
q "\/" p is V11() ext-real V15() Element of the carrier of ()
the L_join of () . (q,p) is V11() ext-real V15() Element of the carrier of ()
max (q,p) is V11() ext-real V15() set
A "/\" (q "\/" p) is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,(q "\/" p)) is V11() ext-real V15() Element of the carrier of ()
min (A,(q "\/" p)) is V11() ext-real V15() set
A "/\" q is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,q) is V11() ext-real V15() Element of the carrier of ()
min (A,q) is V11() ext-real V15() set
A "/\" p is V11() ext-real V15() Element of the carrier of ()
the L_meet of () . (A,p) is V11() ext-real V15() Element of the carrier of ()
min (A,p) is V11() ext-real V15() set
(A "/\" q) "\/" (A "/\" p) is V11() ext-real V15() Element of the carrier of ()
the L_join of () . ((A "/\" q),(A "/\" p)) is V11() ext-real V15() Element of the carrier of ()
max ((A "/\" q),(A "/\" p)) is V11() ext-real V15() set
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
q is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
q is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
p is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
r is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
s is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
q . (r,s) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
() .: (r,s) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p . (r,s) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
q is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
q is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
p is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
r is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
s is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
q . (r,s) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
() .: (r,s) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p . (r,s) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
A is non empty set
q is non empty set
K7(A,q) is set
K6(K7(A,q)) is set
p is Element of A
r is Relation-like A -defined q -valued V21() quasi_total Element of K6(K7(A,q))
dom r is set
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
q is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (p,q) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
r is Element of A
() .: (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (q,p)) is set
() .: (p,q) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (p,q)) is set
((A) . (q,p)) . r is V11() ext-real V15() Element of REAL
(() .: (q,p)) . r is V11() ext-real V15() Element of REAL
q . r is V11() ext-real V15() Element of REAL
p . r is V11() ext-real V15() Element of REAL
() . ((q . r),(p . r)) is V11() ext-real V15() Element of REAL
() . ((p . r),(q . r)) is V11() ext-real V15() Element of REAL
(() .: (p,q)) . r is V11() ext-real V15() Element of REAL
((A) . (p,q)) . r is V11() ext-real V15() Element of REAL
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
q is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (p,q) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
r is Element of A
() .: (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (q,p)) is set
() .: (p,q) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (p,q)) is set
((A) . (q,p)) . r is V11() ext-real V15() Element of REAL
(() .: (q,p)) . r is V11() ext-real V15() Element of REAL
q . r is V11() ext-real V15() Element of REAL
p . r is V11() ext-real V15() Element of REAL
() . ((q . r),(p . r)) is V11() ext-real V15() Element of REAL
() . ((p . r),(q . r)) is V11() ext-real V15() Element of REAL
(() .: (p,q)) . r is V11() ext-real V15() Element of REAL
((A) . (p,q)) . r is V11() ext-real V15() Element of REAL
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
q is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
r is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (((A) . (q,p)),r) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (p,r) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,((A) . (p,r))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
s is Element of A
() .: (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (q,p)) is set
() .: (p,r) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (p,r)) is set
() .: ((() .: (q,p)),r) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: ((() .: (q,p)),r)) is set
() .: (q,(() .: (p,r))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (q,(() .: (p,r)))) is set
((A) . (((A) . (q,p)),r)) . s is V11() ext-real V15() Element of REAL
(A) . ((() .: (q,p)),r) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
((A) . ((() .: (q,p)),r)) . s is V11() ext-real V15() Element of REAL
(() .: ((() .: (q,p)),r)) . s is V11() ext-real V15() Element of REAL
(() .: (q,p)) . s is V11() ext-real V15() Element of REAL
r . s is V11() ext-real V15() Element of REAL
() . (((() .: (q,p)) . s),(r . s)) is V11() ext-real V15() Element of REAL
q . s is V11() ext-real V15() Element of REAL
p . s is V11() ext-real V15() Element of REAL
() . ((q . s),(p . s)) is V11() ext-real V15() Element of REAL
() . ((() . ((q . s),(p . s))),(r . s)) is V11() ext-real V15() Element of REAL
() . ((p . s),(r . s)) is V11() ext-real V15() Element of REAL
() . ((q . s),(() . ((p . s),(r . s)))) is V11() ext-real V15() Element of REAL
(() .: (p,r)) . s is V11() ext-real V15() Element of REAL
() . ((q . s),((() .: (p,r)) . s)) is V11() ext-real V15() Element of REAL
(() .: (q,(() .: (p,r)))) . s is V11() ext-real V15() Element of REAL
(A) . (q,(() .: (p,r))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
((A) . (q,(() .: (p,r)))) . s is V11() ext-real V15() Element of REAL
((A) . (q,((A) . (p,r)))) . s is V11() ext-real V15() Element of REAL
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
q is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
r is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (((A) . (q,p)),r) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (p,r) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,((A) . (p,r))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
s is Element of A
() .: (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (q,p)) is set
() .: (p,r) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (p,r)) is set
() .: ((() .: (q,p)),r) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: ((() .: (q,p)),r)) is set
() .: (q,(() .: (p,r))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (q,(() .: (p,r)))) is set
((A) . (((A) . (q,p)),r)) . s is V11() ext-real V15() Element of REAL
(A) . ((() .: (q,p)),r) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
((A) . ((() .: (q,p)),r)) . s is V11() ext-real V15() Element of REAL
(() .: ((() .: (q,p)),r)) . s is V11() ext-real V15() Element of REAL
(() .: (q,p)) . s is V11() ext-real V15() Element of REAL
r . s is V11() ext-real V15() Element of REAL
() . (((() .: (q,p)) . s),(r . s)) is V11() ext-real V15() Element of REAL
q . s is V11() ext-real V15() Element of REAL
p . s is V11() ext-real V15() Element of REAL
() . ((q . s),(p . s)) is V11() ext-real V15() Element of REAL
() . ((() . ((q . s),(p . s))),(r . s)) is V11() ext-real V15() Element of REAL
() . ((p . s),(r . s)) is V11() ext-real V15() Element of REAL
() . ((q . s),(() . ((p . s),(r . s)))) is V11() ext-real V15() Element of REAL
(() .: (p,r)) . s is V11() ext-real V15() Element of REAL
() . ((q . s),((() .: (p,r)) . s)) is V11() ext-real V15() Element of REAL
(() .: (q,(() .: (p,r)))) . s is V11() ext-real V15() Element of REAL
(A) . (q,(() .: (p,r))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
((A) . (q,(() .: (p,r)))) . s is V11() ext-real V15() Element of REAL
((A) . (q,((A) . (p,r)))) . s is V11() ext-real V15() Element of REAL
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
q is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,((A) . (q,p))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
r is Element of A
() .: (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (q,p)) is set
() .: (q,(() .: (q,p))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (q,(() .: (q,p)))) is set
((A) . (q,((A) . (q,p)))) . r is V11() ext-real V15() Element of REAL
(A) . (q,(() .: (q,p))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
((A) . (q,(() .: (q,p)))) . r is V11() ext-real V15() Element of REAL
(() .: (q,(() .: (q,p)))) . r is V11() ext-real V15() Element of REAL
q . r is V11() ext-real V15() Element of REAL
(() .: (q,p)) . r is V11() ext-real V15() Element of REAL
() . ((q . r),((() .: (q,p)) . r)) is V11() ext-real V15() Element of REAL
p . r is V11() ext-real V15() Element of REAL
() . ((q . r),(p . r)) is V11() ext-real V15() Element of REAL
() . ((q . r),(() . ((q . r),(p . r)))) is V11() ext-real V15() Element of REAL
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
q is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (((A) . (q,p)),q) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,((A) . (q,p))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
q is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (((A) . (q,p)),p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (p,q) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (((A) . (p,q)),p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
q is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (p,q) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,((A) . (p,q))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,((A) . (q,p))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
q is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,((A) . (q,p))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
r is Element of A
() .: (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (q,p)) is set
() .: (q,(() .: (q,p))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (q,(() .: (q,p)))) is set
((A) . (q,((A) . (q,p)))) . r is V11() ext-real V15() Element of REAL
(A) . (q,(() .: (q,p))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
((A) . (q,(() .: (q,p)))) . r is V11() ext-real V15() Element of REAL
(() .: (q,(() .: (q,p)))) . r is V11() ext-real V15() Element of REAL
q . r is V11() ext-real V15() Element of REAL
(() .: (q,p)) . r is V11() ext-real V15() Element of REAL
() . ((q . r),((() .: (q,p)) . r)) is V11() ext-real V15() Element of REAL
p . r is V11() ext-real V15() Element of REAL
() . ((q . r),(p . r)) is V11() ext-real V15() Element of REAL
() . ((q . r),(() . ((q . r),(p . r)))) is V11() ext-real V15() Element of REAL
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
q is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (p,q) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,((A) . (p,q))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,((A) . (q,p))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
q is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (((A) . (q,p)),p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (p,((A) . (q,p))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
q is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (((A) . (q,p)),q) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (p,q) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (((A) . (p,q)),q) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
q is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
p is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
r is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (p,r) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,((A) . (p,r))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (q,r) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
(A) . (((A) . (q,p)),((A) . (q,r))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
s is Element of A
() .: (q,p) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (q,p)) is set
() .: (q,r) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (q,r)) is set
() .: (p,r) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
() .: (q,(() .: (p,r))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: (q,(() .: (p,r)))) is set
() .: ((() .: (q,p)),(() .: (q,r))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
dom (() .: ((() .: (q,p)),(() .: (q,r)))) is set
dom (() .: (p,r)) is set
((A) . (q,((A) . (p,r)))) . s is V11() ext-real V15() Element of REAL
(A) . (q,(() .: (p,r))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
((A) . (q,(() .: (p,r)))) . s is V11() ext-real V15() Element of REAL
(() .: (q,(() .: (p,r)))) . s is V11() ext-real V15() Element of REAL
q . s is V11() ext-real V15() Element of REAL
(() .: (p,r)) . s is V11() ext-real V15() Element of REAL
() . ((q . s),((() .: (p,r)) . s)) is V11() ext-real V15() Element of REAL
p . s is V11() ext-real V15() Element of REAL
r . s is V11() ext-real V15() Element of REAL
() . ((p . s),(r . s)) is V11() ext-real V15() Element of REAL
() . ((q . s),(() . ((p . s),(r . s)))) is V11() ext-real V15() Element of REAL
() . ((q . s),(p . s)) is V11() ext-real V15() Element of REAL
() . ((q . s),(r . s)) is V11() ext-real V15() Element of REAL
() . ((() . ((q . s),(p . s))),(() . ((q . s),(r . s)))) is V11() ext-real V15() Element of REAL
(() .: (q,p)) . s is V11() ext-real V15() Element of REAL
() . (((() .: (q,p)) . s),(() . ((q . s),(r . s)))) is V11() ext-real V15() Element of REAL
(() .: (q,r)) . s is V11() ext-real V15() Element of REAL
() . (((() .: (q,p)) . s),((() .: (q,r)) . s)) is V11() ext-real V15() Element of REAL
(() .: ((() .: (q,p)),(() .: (q,r)))) . s is V11() ext-real V15() Element of REAL
(A) . ((() .: (q,p)),(() .: (q,r))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
((A) . ((() .: (q,p)),(() .: (q,r)))) . s is V11() ext-real V15() Element of REAL
(A) . (((A) . (q,p)),(() .: (q,r))) is Relation-like A -defined REAL -valued V21() quasi_total Element of Funcs (A,REAL)
((A) . (((A) . (q,p)),(() .: (q,r)))) . s is V11() ext-real V15() Element of REAL
((A) . (((A) . (q,p)),((A) . (q,r)))) . s is V11() ext-real V15() Element of REAL
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
LattStr(# (Funcs (A,REAL)),(A),(A) #) is non empty strict LattStr
the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #) is set
q is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
p is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
r is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
p "\/" r is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
the L_join of LattStr(# (Funcs (A,REAL)),(A),(A) #) is Relation-like K7( the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)) -defined the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #) -valued V21() quasi_total Element of K6(K7(K7( the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)))
K7( the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)) is set
K7(K7( the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)) is set
K6(K7(K7( the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #))) is set
the L_join of LattStr(# (Funcs (A,REAL)),(A),(A) #) . (p,r) is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
q "\/" (p "\/" r) is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
the L_join of LattStr(# (Funcs (A,REAL)),(A),(A) #) . (q,(p "\/" r)) is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
q "\/" p is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
the L_join of LattStr(# (Funcs (A,REAL)),(A),(A) #) . (q,p) is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
(q "\/" p) "\/" r is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
the L_join of LattStr(# (Funcs (A,REAL)),(A),(A) #) . ((q "\/" p),r) is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
LattStr(# (Funcs (A,REAL)),(A),(A) #) is non empty strict LattStr
the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #) is set
q is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
p is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
r is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
p "/\" r is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
the L_meet of LattStr(# (Funcs (A,REAL)),(A),(A) #) is Relation-like K7( the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)) -defined the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #) -valued V21() quasi_total Element of K6(K7(K7( the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)))
K7( the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)) is set
K7(K7( the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)) is set
K6(K7(K7( the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)), the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #))) is set
the L_meet of LattStr(# (Funcs (A,REAL)),(A),(A) #) . (p,r) is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
q "/\" (p "/\" r) is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
the L_meet of LattStr(# (Funcs (A,REAL)),(A),(A) #) . (q,(p "/\" r)) is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
q "/\" p is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
the L_meet of LattStr(# (Funcs (A,REAL)),(A),(A) #) . (q,p) is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
(q "/\" p) "/\" r is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
the L_meet of LattStr(# (Funcs (A,REAL)),(A),(A) #) . ((q "/\" p),r) is Element of the carrier of LattStr(# (Funcs (A,REAL)),(A),(A) #)
A is non empty set
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
LattStr(# (Funcs (A,REAL)),(A),(A) #) is non empty strict LattStr
A is non empty set
(A) is non empty strict LattStr
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
LattStr(# (Funcs (A,REAL)),(A),(A) #) is non empty strict LattStr
q is non empty LattStr
the carrier of q is set
p is Element of the carrier of q
r is Element of the carrier of q
p "\/" r is Element of the carrier of q
the L_join of q is Relation-like K7( the carrier of q, the carrier of q) -defined the carrier of q -valued V21() quasi_total Element of K6(K7(K7( the carrier of q, the carrier of q), the carrier of q))
K7( the carrier of q, the carrier of q) is set
K7(K7( the carrier of q, the carrier of q), the carrier of q) is set
K6(K7(K7( the carrier of q, the carrier of q), the carrier of q)) is set
the L_join of q . (p,r) is Element of the carrier of q
r "\/" p is Element of the carrier of q
the L_join of q . (r,p) is Element of the carrier of q
p is Element of the carrier of q
r is Element of the carrier of q
s is Element of the carrier of q
r "\/" s is Element of the carrier of q
the L_join of q is Relation-like K7( the carrier of q, the carrier of q) -defined the carrier of q -valued V21() quasi_total Element of K6(K7(K7( the carrier of q, the carrier of q), the carrier of q))
K7( the carrier of q, the carrier of q) is set
K7(K7( the carrier of q, the carrier of q), the carrier of q) is set
K6(K7(K7( the carrier of q, the carrier of q), the carrier of q)) is set
the L_join of q . (r,s) is Element of the carrier of q
p "\/" (r "\/" s) is Element of the carrier of q
the L_join of q . (p,(r "\/" s)) is Element of the carrier of q
p "\/" r is Element of the carrier of q
the L_join of q . (p,r) is Element of the carrier of q
(p "\/" r) "\/" s is Element of the carrier of q
the L_join of q . ((p "\/" r),s) is Element of the carrier of q
p is Element of the carrier of q
r is Element of the carrier of q
p "/\" r is Element of the carrier of q
the L_meet of q is Relation-like K7( the carrier of q, the carrier of q) -defined the carrier of q -valued V21() quasi_total Element of K6(K7(K7( the carrier of q, the carrier of q), the carrier of q))
K7( the carrier of q, the carrier of q) is set
K7(K7( the carrier of q, the carrier of q), the carrier of q) is set
K6(K7(K7( the carrier of q, the carrier of q), the carrier of q)) is set
the L_meet of q . (p,r) is Element of the carrier of q
(p "/\" r) "\/" r is Element of the carrier of q
the L_join of q is Relation-like K7( the carrier of q, the carrier of q) -defined the carrier of q -valued V21() quasi_total Element of K6(K7(K7( the carrier of q, the carrier of q), the carrier of q))
the L_join of q . ((p "/\" r),r) is Element of the carrier of q
p is Element of the carrier of q
r is Element of the carrier of q
p "/\" r is Element of the carrier of q
the L_meet of q is Relation-like K7( the carrier of q, the carrier of q) -defined the carrier of q -valued V21() quasi_total Element of K6(K7(K7( the carrier of q, the carrier of q), the carrier of q))
K7( the carrier of q, the carrier of q) is set
K7(K7( the carrier of q, the carrier of q), the carrier of q) is set
K6(K7(K7( the carrier of q, the carrier of q), the carrier of q)) is set
the L_meet of q . (p,r) is Element of the carrier of q
r "/\" p is Element of the carrier of q
the L_meet of q . (r,p) is Element of the carrier of q
p is Element of the carrier of q
r is Element of the carrier of q
s is Element of the carrier of q
r "/\" s is Element of the carrier of q
the L_meet of q is Relation-like K7( the carrier of q, the carrier of q) -defined the carrier of q -valued V21() quasi_total Element of K6(K7(K7( the carrier of q, the carrier of q), the carrier of q))
K7( the carrier of q, the carrier of q) is set
K7(K7( the carrier of q, the carrier of q), the carrier of q) is set
K6(K7(K7( the carrier of q, the carrier of q), the carrier of q)) is set
the L_meet of q . (r,s) is Element of the carrier of q
p "/\" (r "/\" s) is Element of the carrier of q
the L_meet of q . (p,(r "/\" s)) is Element of the carrier of q
p "/\" r is Element of the carrier of q
the L_meet of q . (p,r) is Element of the carrier of q
(p "/\" r) "/\" s is Element of the carrier of q
the L_meet of q . ((p "/\" r),s) is Element of the carrier of q
p is Element of the carrier of q
r is Element of the carrier of q
p "\/" r is Element of the carrier of q
the L_join of q is Relation-like K7( the carrier of q, the carrier of q) -defined the carrier of q -valued V21() quasi_total Element of K6(K7(K7( the carrier of q, the carrier of q), the carrier of q))
K7( the carrier of q, the carrier of q) is set
K7(K7( the carrier of q, the carrier of q), the carrier of q) is set
K6(K7(K7( the carrier of q, the carrier of q), the carrier of q)) is set
the L_join of q . (p,r) is Element of the carrier of q
p "/\" (p "\/" r) is Element of the carrier of q
the L_meet of q is Relation-like K7( the carrier of q, the carrier of q) -defined the carrier of q -valued V21() quasi_total Element of K6(K7(K7( the carrier of q, the carrier of q), the carrier of q))
the L_meet of q . (p,(p "\/" r)) is Element of the carrier of q
A is non empty set
(A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
LattStr(# (Funcs (A,REAL)),(A),(A) #) is non empty strict LattStr
the carrier of (A) is set
q is Element of the carrier of (A)
p is Element of the carrier of (A)
(A) . (q,p) is set
(A) . (p,q) is set
p "\/" q is Element of the carrier of (A)
the L_join of (A) is Relation-like K7( the carrier of (A), the carrier of (A)) -defined the carrier of (A) -valued V21() quasi_total Element of K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)))
K7( the carrier of (A), the carrier of (A)) is set
K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)) is set
K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A))) is set
the L_join of (A) . (p,q) is Element of the carrier of (A)
A is non empty set
(A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
LattStr(# (Funcs (A,REAL)),(A),(A) #) is non empty strict LattStr
the carrier of (A) is set
q is Element of the carrier of (A)
p is Element of the carrier of (A)
(A) . (q,p) is set
(A) . (p,q) is set
p "/\" q is Element of the carrier of (A)
the L_meet of (A) is Relation-like K7( the carrier of (A), the carrier of (A)) -defined the carrier of (A) -valued V21() quasi_total Element of K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)))
K7( the carrier of (A), the carrier of (A)) is set
K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)) is set
K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A))) is set
the L_meet of (A) . (p,q) is Element of the carrier of (A)
A is non empty set
(A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
LattStr(# (Funcs (A,REAL)),(A),(A) #) is non empty strict LattStr
the carrier of (A) is set
q is Element of the carrier of (A)
p is Element of the carrier of (A)
(A) . (q,p) is set
(A) . (p,q) is set
r is Element of the carrier of (A)
(A) . (p,r) is set
(A) . (q,((A) . (p,r))) is set
(A) . (((A) . (p,r)),q) is set
(A) . (((A) . (q,p)),r) is set
(A) . (((A) . (p,q)),r) is set
(A) . (r,q) is set
(A) . (((A) . (r,q)),p) is set
(A) . (r,p) is set
(A) . (((A) . (r,p)),q) is set
(A) . (q,r) is set
(A) . (((A) . (q,r)),p) is set
p "\/" r is Element of the carrier of (A)
the L_join of (A) is Relation-like K7( the carrier of (A), the carrier of (A)) -defined the carrier of (A) -valued V21() quasi_total Element of K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)))
K7( the carrier of (A), the carrier of (A)) is set
K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)) is set
K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A))) is set
the L_join of (A) . (p,r) is Element of the carrier of (A)
(p "\/" r) "\/" q is Element of the carrier of (A)
the L_join of (A) . ((p "\/" r),q) is Element of the carrier of (A)
q "\/" (p "\/" r) is Element of the carrier of (A)
the L_join of (A) . (q,(p "\/" r)) is Element of the carrier of (A)
p "\/" q is Element of the carrier of (A)
the L_join of (A) . (p,q) is Element of the carrier of (A)
(p "\/" q) "\/" r is Element of the carrier of (A)
the L_join of (A) . ((p "\/" q),r) is Element of the carrier of (A)
r "\/" q is Element of the carrier of (A)
the L_join of (A) . (r,q) is Element of the carrier of (A)
(r "\/" q) "\/" p is Element of the carrier of (A)
the L_join of (A) . ((r "\/" q),p) is Element of the carrier of (A)
A is non empty set
(A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
LattStr(# (Funcs (A,REAL)),(A),(A) #) is non empty strict LattStr
the carrier of (A) is set
q is Element of the carrier of (A)
p is Element of the carrier of (A)
(A) . (q,p) is set
(A) . (p,q) is set
r is Element of the carrier of (A)
(A) . (p,r) is set
(A) . (q,((A) . (p,r))) is set
(A) . (((A) . (p,r)),q) is set
(A) . (((A) . (q,p)),r) is set
(A) . (((A) . (p,q)),r) is set
(A) . (r,q) is set
(A) . (((A) . (r,q)),p) is set
(A) . (r,p) is set
(A) . (((A) . (r,p)),q) is set
(A) . (q,r) is set
(A) . (((A) . (q,r)),p) is set
p "/\" r is Element of the carrier of (A)
the L_meet of (A) is Relation-like K7( the carrier of (A), the carrier of (A)) -defined the carrier of (A) -valued V21() quasi_total Element of K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)))
K7( the carrier of (A), the carrier of (A)) is set
K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)) is set
K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A))) is set
the L_meet of (A) . (p,r) is Element of the carrier of (A)
(p "/\" r) "/\" q is Element of the carrier of (A)
the L_meet of (A) . ((p "/\" r),q) is Element of the carrier of (A)
q "/\" (p "/\" r) is Element of the carrier of (A)
the L_meet of (A) . (q,(p "/\" r)) is Element of the carrier of (A)
p "/\" q is Element of the carrier of (A)
the L_meet of (A) . (p,q) is Element of the carrier of (A)
(p "/\" q) "/\" r is Element of the carrier of (A)
the L_meet of (A) . ((p "/\" q),r) is Element of the carrier of (A)
r "/\" q is Element of the carrier of (A)
the L_meet of (A) . (r,q) is Element of the carrier of (A)
(r "/\" q) "/\" p is Element of the carrier of (A)
the L_meet of (A) . ((r "/\" q),p) is Element of the carrier of (A)
A is non empty set
(A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
LattStr(# (Funcs (A,REAL)),(A),(A) #) is non empty strict LattStr
the carrier of (A) is set
q is Element of the carrier of (A)
p is Element of the carrier of (A)
(A) . (q,p) is set
(A) . (((A) . (q,p)),p) is set
(A) . (p,((A) . (q,p))) is set
(A) . (p,q) is set
(A) . (p,((A) . (p,q))) is set
(A) . (((A) . (p,q)),p) is set
q "/\" p is Element of the carrier of (A)
the L_meet of (A) is Relation-like K7( the carrier of (A), the carrier of (A)) -defined the carrier of (A) -valued V21() quasi_total Element of K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)))
K7( the carrier of (A), the carrier of (A)) is set
K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)) is set
K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A))) is set
the L_meet of (A) . (q,p) is Element of the carrier of (A)
(q "/\" p) "\/" p is Element of the carrier of (A)
the L_join of (A) is Relation-like K7( the carrier of (A), the carrier of (A)) -defined the carrier of (A) -valued V21() quasi_total Element of K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)))
the L_join of (A) . ((q "/\" p),p) is Element of the carrier of (A)
p "/\" q is Element of the carrier of (A)
the L_meet of (A) . (p,q) is Element of the carrier of (A)
(A) . (p,(p "/\" q)) is set
A is non empty set
(A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
LattStr(# (Funcs (A,REAL)),(A),(A) #) is non empty strict LattStr
the carrier of (A) is set
q is Element of the carrier of (A)
p is Element of the carrier of (A)
(A) . (q,p) is set
(A) . (q,((A) . (q,p))) is set
(A) . (p,q) is set
(A) . (((A) . (p,q)),q) is set
(A) . (q,((A) . (p,q))) is set
(A) . (((A) . (q,p)),q) is set
p "\/" q is Element of the carrier of (A)
the L_join of (A) is Relation-like K7( the carrier of (A), the carrier of (A)) -defined the carrier of (A) -valued V21() quasi_total Element of K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)))
K7( the carrier of (A), the carrier of (A)) is set
K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)) is set
K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A))) is set
the L_join of (A) . (p,q) is Element of the carrier of (A)
(A) . ((p "\/" q),q) is set
q "\/" p is Element of the carrier of (A)
the L_join of (A) . (q,p) is Element of the carrier of (A)
q "/\" (q "\/" p) is Element of the carrier of (A)
the L_meet of (A) is Relation-like K7( the carrier of (A), the carrier of (A)) -defined the carrier of (A) -valued V21() quasi_total Element of K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)))
the L_meet of (A) . (q,(q "\/" p)) is Element of the carrier of (A)
A is non empty set
(A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
LattStr(# (Funcs (A,REAL)),(A),(A) #) is non empty strict LattStr
the carrier of (A) is set
q is Element of the carrier of (A)
p is Element of the carrier of (A)
r is Element of the carrier of (A)
(A) . (p,r) is set
(A) . (q,((A) . (p,r))) is set
(A) . (q,p) is set
(A) . (q,r) is set
(A) . (((A) . (q,p)),((A) . (q,r))) is set
A is non empty set
(A) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Funcs (A,REAL) is non empty FUNCTION_DOMAIN of A, REAL
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
K7((Funcs (A,REAL)),(Funcs (A,REAL))) is set
K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))) is set
K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL)))) is set
(A) is Relation-like K7((Funcs (A,REAL)),(Funcs (A,REAL))) -defined Funcs (A,REAL) -valued V21() quasi_total Element of K6(K7(K7((Funcs (A,REAL)),(Funcs (A,REAL))),(Funcs (A,REAL))))
LattStr(# (Funcs (A,REAL)),(A),(A) #) is non empty strict LattStr
the carrier of (A) is set
q is Element of the carrier of (A)
p is Element of the carrier of (A)
r is Element of the carrier of (A)
p "\/" r is Element of the carrier of (A)
the L_join of (A) is Relation-like K7( the carrier of (A), the carrier of (A)) -defined the carrier of (A) -valued V21() quasi_total Element of K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)))
K7( the carrier of (A), the carrier of (A)) is set
K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)) is set
K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A))) is set
the L_join of (A) . (p,r) is Element of the carrier of (A)
q "/\" (p "\/" r) is Element of the carrier of (A)
the L_meet of (A) is Relation-like K7( the carrier of (A), the carrier of (A)) -defined the carrier of (A) -valued V21() quasi_total Element of K6(K7(K7( the carrier of (A), the carrier of (A)), the carrier of (A)))
the L_meet of (A) . (q,(p "\/" r)) is Element of the carrier of (A)
q "/\" p is Element of the carrier of (A)
the L_meet of (A) . (q,p) is Element of the carrier of (A)
q "/\" r is Element of the carrier of (A)
the L_meet of (A) . (q,r) is Element of the carrier of (A)
(q "/\" p) "\/" (q "/\" r) is Element of the carrier of (A)
the L_join of (A) . ((q "/\" p),(q "/\" r)) is Element of the carrier of (A)