REAL is V267() V268() V269() V273() V283() V284() V286() set
NAT is non empty non trivial V25() non finite cardinal limit_cardinal countable denumerable V267() V268() V269() V270() V271() V272() V273() V281() V283() Element of bool REAL
bool REAL is non empty set
NAT is non empty non trivial V25() non finite cardinal limit_cardinal countable denumerable V267() V268() V269() V270() V271() V272() V273() V281() V283() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K211() is set
{} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
RAT is V267() V268() V269() V270() V273() set
{{}} is functional non empty trivial finite V34() 1 -element with_common_domain countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
K189({{}}) is M8({{}})
[:K189({{}}),{{}}:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
INT is V267() V268() V269() V270() V271() V273() set
bool [:K189({{}}),{{}}:] is non empty set
K98(K189({{}}),{{}}) is functional non empty set
{{},1} is non empty finite V34() countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
COMPLEX is V267() V273() set
[:COMPLEX,COMPLEX:] is Relation-like complex-valued set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:COMPLEX,REAL:] is non empty set
0 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() V250() V251() ext-real non positive non negative V255() V256() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() Element of NAT
2 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
card NAT is non empty non trivial V25() non finite cardinal set
[:NAT,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty set
id {{}} is Relation-like {{}} -defined {{}} -valued RAT -valued INT -valued Function-like one-to-one non empty V19({{}}) V20({{}},{{}}) V21({{}}) V22({{}},{{}}) finite countable Function-yielding V44() reflexive symmetric antisymmetric transitive complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:{{}},{{}}:]
[:{{}},{{}}:] is Relation-like RAT -valued INT -valued non empty finite countable complex-valued ext-real-valued real-valued natural-valued set
bool [:{{}},{{}}:] is non empty finite V34() countable set
RelStr(# {{}},(id {{}}) #) is non empty strict V81() reflexive transitive antisymmetric non void RelStr
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,NAT:] is non empty non trivial non finite set
R is Relation-like Function-like set
dom R is set
IR is set
{IR} is non empty trivial finite 1 -element countable set
R . IR is set
IR .--> (R . IR) is Relation-like {IR} -defined Function-like one-to-one finite countable set
{IR} --> (R . IR) is Relation-like {IR} -defined {(R . IR)} -valued Function-like constant non empty V19({IR}) V20({IR},{(R . IR)}) finite countable Element of bool [:{IR},{(R . IR)}:]
{(R . IR)} is non empty trivial finite 1 -element countable set
[:{IR},{(R . IR)}:] is Relation-like non empty finite countable set
bool [:{IR},{(R . IR)}:] is non empty finite V34() countable set
dom (IR .--> (R . IR)) is trivial finite countable Element of bool {IR}
bool {IR} is non empty finite V34() countable set
CR is set
f is set
[CR,f] is V13() non empty set
{CR,f} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,f},{CR}} is non empty finite V34() countable set
(IR .--> (R . IR)) . CR is set
R . CR is set
R is V25() V29() finite cardinal countable ext-real non negative set
R + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
{R} is non empty trivial finite V34() 1 -element countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
R \/ {R} is non empty finite countable set
F1() is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
F2() is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
{ F3(b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( not b1 <= F1() & b1 <= F2() & P1[b1] ) } is set
{ F3(b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( F1() <= b1 & b1 <= F2() & P1[b1] ) } is set
CR is set
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
F3(f) is set
R is non empty non trivial non finite set
[:NAT,R:] is Relation-like non empty non trivial non finite set
bool [:NAT,R:] is non empty non trivial non finite set
card NAT is non empty non trivial V25() non finite cardinal set
card R is non empty non trivial V25() non finite cardinal set
IR is Relation-like Function-like set
dom IR is set
rng IR is set
CR is set
IR . CR is set
CR is Relation-like NAT -defined R -valued Function-like non empty V19( NAT ) V20( NAT ,R) Element of bool [:NAT,R:]
R is RelStr
the carrier of R is set
[:NAT, the carrier of R:] is Relation-like set
bool [:NAT, the carrier of R:] is non empty set
R is RelStr
the carrier of R is set
[:NAT, the carrier of R:] is Relation-like set
bool [:NAT, the carrier of R:] is non empty set
R is non empty transitive RelStr
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
IR is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
CR is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . CR is Element of the carrier of R
IR . 0 is Element of the carrier of R
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . f is Element of the carrier of R
f + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
IR . (f + 1) is Element of the carrier of R
[(IR . f),(IR . (f + 1))] is V13() non empty Element of the carrier of [:R,R:]
[:R,R:] is non empty strict transitive RelStr
the carrier of [:R,R:] is non empty set
{(IR . f),(IR . (f + 1))} is non empty finite countable set
{(IR . f)} is non empty trivial finite 1 -element countable set
{{(IR . f),(IR . (f + 1))},{(IR . f)}} is non empty finite V34() countable set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
QOE is Element of the carrier of R
R is non empty RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is non empty set
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
f is set
QOE is set
S is Element of the carrier of R
f9 is Element of the carrier of R
[f,QOE] is V13() non empty set
{f,QOE} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,QOE},{f}} is non empty finite V34() countable set
[QOE,f] is V13() non empty set
{QOE,f} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,f},{QOE}} is non empty finite V34() countable set
f is Element of the carrier of R
QOE is Element of the carrier of R
[f,QOE] is V13() non empty Element of the carrier of [:R,R:]
[:R,R:] is non empty strict RelStr
the carrier of [:R,R:] is non empty set
{f,QOE} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,QOE},{f}} is non empty finite V34() countable set
[QOE,f] is V13() non empty Element of the carrier of [:R,R:]
{QOE,f} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,f},{QOE}} is non empty finite V34() countable set
R is RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is set
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
IR is set
CR is set
the InternalRel of R -Seg CR is set
( the InternalRel of R -Seg CR) /\ IR is set
QOE is set
[QOE,CR] is V13() non empty set
{QOE,CR} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,CR},{QOE}} is non empty finite V34() countable set
QOE is set
[QOE,CR] is V13() non empty set
{QOE,CR} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,CR},{QOE}} is non empty finite V34() countable set
QOE is set
[QOE,CR] is V13() non empty set
{QOE,CR} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,CR},{QOE}} is non empty finite V34() countable set
R is non empty transitive antisymmetric RelStr
the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
IR is Element of the carrier of R
the InternalRel of R -Seg IR is set
f is set
( the InternalRel of R -Seg IR) /\ f is set
CR is set
[CR,IR] is V13() non empty set
{CR,IR} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,IR},{CR}} is non empty finite V34() countable set
n is set
[n,CR] is V13() non empty set
{n,CR} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,CR},{n}} is non empty finite V34() countable set
n is set
[n,CR] is V13() non empty set
{n,CR} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,CR},{n}} is non empty finite V34() countable set
[n,IR] is V13() non empty set
{n,IR} is non empty finite countable set
{{n,IR},{n}} is non empty finite V34() countable set
f9 is Element of the carrier of R
n is set
[n,CR] is V13() non empty set
{n,CR} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,CR},{n}} is non empty finite V34() countable set
R is RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
f is set
[f,f] is V13() non empty set
{f,f} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,f},{f}} is non empty finite V34() countable set
dom ( the InternalRel of R /\ ( the InternalRel of R ~)) is Element of bool the carrier of R
bool the carrier of R is non empty set
field ( the InternalRel of R /\ ( the InternalRel of R ~)) is set
f is set
QOE is set
[f,QOE] is V13() non empty set
{f,QOE} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,QOE},{f}} is non empty finite V34() countable set
[QOE,f] is V13() non empty set
{QOE,f} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,f},{QOE}} is non empty finite V34() countable set
f is set
QOE is set
S is set
[f,QOE] is V13() non empty set
{f,QOE} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,QOE},{f}} is non empty finite V34() countable set
[QOE,S] is V13() non empty set
{QOE,S} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,S},{QOE}} is non empty finite V34() countable set
[f,S] is V13() non empty set
{f,S} is non empty finite countable set
{{f,S},{f}} is non empty finite V34() countable set
R is RelStr
the carrier of R is set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
IR is Element of the carrier of R
CR is Element of the carrier of R
Class ((R),CR) is Element of bool the carrier of R
bool the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[IR,CR] is V13() non empty set
{IR,CR} is non empty finite countable set
{IR} is non empty trivial finite 1 -element countable set
{{IR,CR},{IR}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[CR,IR] is V13() non empty set
{CR,IR} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,IR},{CR}} is non empty finite V34() countable set
R is RelStr
the carrier of R is set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
Class (R) is with_non-empty_elements a_partition of the carrier of R
[:(Class (R)),(Class (R)):] is Relation-like set
bool [:(Class (R)),(Class (R)):] is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
f is Relation-like Class (R) -defined Class (R) -valued Element of bool [:(Class (R)),(Class (R)):]
QOE is set
S is set
[QOE,S] is V13() non empty set
{QOE,S} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,S},{QOE}} is non empty finite V34() countable set
f9 is Element of the carrier of R
Class ((R),f9) is Element of bool the carrier of R
bool the carrier of R is non empty set
n is Element of the carrier of R
Class ((R),n) is Element of bool the carrier of R
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of R is non empty set
{ [(Class ((R),b1)),(Class ((R),b2))] where b1, b2 is Element of the carrier of f : b1 <= b2 } is set
[:(Class (R)),(Class (R)):] is Relation-like bool the carrier of R -defined bool the carrier of R -valued Element of bool [:(bool the carrier of R),(bool the carrier of R):]
[:(bool the carrier of R),(bool the carrier of R):] is Relation-like non empty set
bool [:(bool the carrier of R),(bool the carrier of R):] is non empty set
f9 is set
n is Element of the carrier of f
Class ((R),n) is Element of bool the carrier of R
n1 is Element of the carrier of f
Class ((R),n1) is Element of bool the carrier of R
[(Class ((R),n)),(Class ((R),n1))] is V13() non empty Element of [:(bool the carrier of R),(bool the carrier of R):]
{(Class ((R),n)),(Class ((R),n1))} is non empty finite countable set
{(Class ((R),n))} is non empty trivial finite 1 -element countable set
{{(Class ((R),n)),(Class ((R),n1))},{(Class ((R),n))}} is non empty finite V34() countable set
f9 is Relation-like Class (R) -defined Class (R) -valued Element of bool [:(Class (R)),(Class (R)):]
n is set
n1 is set
[n,n1] is V13() non empty set
{n,n1} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,n1},{n}} is non empty finite V34() countable set
l is Element of the carrier of R
Class ((R),l) is Element of bool the carrier of R
k is Element of the carrier of R
Class ((R),k) is Element of bool the carrier of R
[(Class ((R),l)),(Class ((R),k))] is V13() non empty Element of [:(bool the carrier of R),(bool the carrier of R):]
{(Class ((R),l)),(Class ((R),k))} is non empty finite countable set
{(Class ((R),l))} is non empty trivial finite 1 -element countable set
{{(Class ((R),l)),(Class ((R),k))},{(Class ((R),l))}} is non empty finite V34() countable set
a is Element of the carrier of R
b is Element of the carrier of R
S is Element of the carrier of R
Class ((R),S) is Element of bool the carrier of R
CP9 is Element of the carrier of R
Class ((R),CP9) is Element of bool the carrier of R
l is Element of the carrier of R
Class ((R),l) is Element of bool the carrier of R
k is Element of the carrier of R
Class ((R),k) is Element of bool the carrier of R
IR is Relation-like Class (R) -defined Class (R) -valued Element of bool [:(Class (R)),(Class (R)):]
CR is Relation-like Class (R) -defined Class (R) -valued Element of bool [:(Class (R)),(Class (R)):]
f is set
S is set
f9 is set
[S,f9] is V13() non empty set
{S,f9} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,f9},{S}} is non empty finite V34() countable set
n is Element of the carrier of R
Class ((R),n) is Element of bool the carrier of R
bool the carrier of R is non empty set
n1 is Element of the carrier of R
Class ((R),n1) is Element of bool the carrier of R
S is set
f9 is set
[S,f9] is V13() non empty set
{S,f9} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,f9},{S}} is non empty finite V34() countable set
n is Element of the carrier of R
Class ((R),n) is Element of bool the carrier of R
bool the carrier of R is non empty set
n1 is Element of the carrier of R
Class ((R),n1) is Element of bool the carrier of R
R is RelStr
(R) is Relation-like Class (R) -defined Class (R) -valued Element of bool [:(Class (R)),(Class (R)):]
the carrier of R is set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
Class (R) is with_non-empty_elements a_partition of the carrier of R
[:(Class (R)),(Class (R)):] is Relation-like set
bool [:(Class (R)),(Class (R)):] is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
f is set
[f,f] is V13() non empty set
{f,f} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,f},{f}} is non empty finite V34() countable set
QOE is set
Class ((R),QOE) is Element of bool the carrier of R
bool the carrier of R is non empty set
[QOE,QOE] is V13() non empty set
{QOE,QOE} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,QOE},{QOE}} is non empty finite V34() countable set
S is Element of the carrier of R
f is set
QOE is set
S is set
[f,QOE] is V13() non empty set
{f,QOE} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,QOE},{f}} is non empty finite V34() countable set
[QOE,S] is V13() non empty set
{QOE,S} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,S},{QOE}} is non empty finite V34() countable set
[f,S] is V13() non empty set
{f,S} is non empty finite countable set
{{f,S},{f}} is non empty finite V34() countable set
f9 is Element of the carrier of R
Class ((R),f9) is Element of bool the carrier of R
bool the carrier of R is non empty set
n is Element of the carrier of R
Class ((R),n) is Element of bool the carrier of R
n1 is Element of the carrier of R
Class ((R),n1) is Element of bool the carrier of R
l is Element of the carrier of R
Class ((R),l) is Element of bool the carrier of R
[f9,n] is V13() non empty set
{f9,n} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n},{f9}} is non empty finite V34() countable set
[n1,l] is V13() non empty set
{n1,l} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,l},{n1}} is non empty finite V34() countable set
k is set
Class ((R),k) is Element of bool the carrier of R
[n,n1] is V13() non empty set
{n,n1} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,n1},{n}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
k is set
Class ((R),k) is Element of bool the carrier of R
[f9,l] is V13() non empty set
{f9,l} is non empty finite countable set
{{f9,l},{f9}} is non empty finite V34() countable set
k is set
Class ((R),k) is Element of bool the carrier of R
f is set
QOE is set
[f,QOE] is V13() non empty set
{f,QOE} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,QOE},{f}} is non empty finite V34() countable set
[QOE,f] is V13() non empty set
{QOE,f} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,f},{QOE}} is non empty finite V34() countable set
S is Element of the carrier of R
Class ((R),S) is Element of bool the carrier of R
bool the carrier of R is non empty set
f9 is Element of the carrier of R
Class ((R),f9) is Element of bool the carrier of R
n is Element of the carrier of R
Class ((R),n) is Element of bool the carrier of R
n1 is Element of the carrier of R
Class ((R),n1) is Element of bool the carrier of R
[S,f9] is V13() non empty set
{S,f9} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,f9},{S}} is non empty finite V34() countable set
[n,n1] is V13() non empty set
{n,n1} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,n1},{n}} is non empty finite V34() countable set
l is set
Class ((R),l) is Element of bool the carrier of R
l is set
Class ((R),l) is Element of bool the carrier of R
[S,n1] is V13() non empty set
{S,n1} is non empty finite countable set
{{S,n1},{S}} is non empty finite V34() countable set
l is set
Class ((R),l) is Element of bool the carrier of R
l is set
Class ((R),l) is Element of bool the carrier of R
[f9,n] is V13() non empty set
{f9,n} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n},{f9}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[n1,S] is V13() non empty set
{n1,S} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,S},{n1}} is non empty finite V34() countable set
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
l is set
Class ((R),l) is Element of bool the carrier of R
[f9,S] is V13() non empty set
{f9,S} is non empty finite countable set
{{f9,S},{f9}} is non empty finite V34() countable set
l is set
Class ((R),l) is Element of bool the carrier of R
R is non empty RelStr
(R) is Relation-like Class (R) -defined Class (R) -valued Element of bool [:(Class (R)),(Class (R)):]
the carrier of R is non empty set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
Class (R) is non empty with_non-empty_elements a_partition of the carrier of R
[:(Class (R)),(Class (R)):] is Relation-like non empty set
bool [:(Class (R)),(Class (R)):] is non empty set
CR is set
f is set
[CR,f] is V13() non empty set
{CR,f} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,f},{CR}} is non empty finite V34() countable set
[f,CR] is V13() non empty set
{f,CR} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,CR},{f}} is non empty finite V34() countable set
QOE is set
Class ((R),QOE) is Element of bool the carrier of R
bool the carrier of R is non empty set
S is set
Class ((R),S) is Element of bool the carrier of R
f9 is Element of the carrier of R
n is Element of the carrier of R
R is Relation-like set
R ~ is Relation-like set
R \ (R ~) is Relation-like Element of bool R
bool R is non empty set
R is Relation-like set
(R) is Relation-like set
R ~ is Relation-like set
R \ (R ~) is Relation-like Element of bool R
bool R is non empty set
IR is set
field (R) is set
CR is set
[IR,CR] is V13() non empty set
{IR,CR} is non empty finite countable set
{IR} is non empty trivial finite 1 -element countable set
{{IR,CR},{IR}} is non empty finite V34() countable set
[CR,IR] is V13() non empty set
{CR,IR} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,IR},{CR}} is non empty finite V34() countable set
R is set
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
IR is Relation-like R -defined R -valued Element of bool [:R,R:]
(IR) is Relation-like asymmetric set
IR ~ is Relation-like set
IR \ (IR ~) is Relation-like R -defined R -valued Element of bool IR
bool IR is non empty set
IR ~ is Relation-like R -defined R -valued Element of bool [:R,R:]
IR \ (IR ~) is Relation-like R -defined R -valued Element of bool [:R,R:]
R is RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is strict RelStr
R is non empty RelStr
(R) is strict RelStr
the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
R is transitive RelStr
(R) is strict RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is strict RelStr
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is set
[: the carrier of (R), the carrier of (R):] is Relation-like set
bool [: the carrier of (R), the carrier of (R):] is non empty set
S is set
f9 is set
n is set
[S,f9] is V13() non empty set
{S,f9} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,f9},{S}} is non empty finite V34() countable set
[f9,n] is V13() non empty set
{f9,n} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n},{f9}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[S,n] is V13() non empty set
{S,n} is non empty finite countable set
{{S,n},{S}} is non empty finite V34() countable set
[n,S] is V13() non empty set
{n,S} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,S},{n}} is non empty finite V34() countable set
[f9,S] is V13() non empty set
{f9,S} is non empty finite countable set
{{f9,S},{f9}} is non empty finite V34() countable set
R is RelStr
(R) is strict RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is strict RelStr
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is set
[: the carrier of (R), the carrier of (R):] is Relation-like set
bool [: the carrier of (R), the carrier of (R):] is non empty set
QOE is set
S is set
[QOE,S] is V13() non empty set
{QOE,S} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,S},{QOE}} is non empty finite V34() countable set
[S,QOE] is V13() non empty set
{S,QOE} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,QOE},{S}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
R is non empty V81() reflexive transitive antisymmetric non void RelStr
the carrier of R is non empty set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued non empty V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive antisymmetric transitive Element of bool [: the carrier of R, the carrier of R:]
f is Element of the carrier of R
Class ((R),f) is Element of bool the carrier of R
bool the carrier of R is non empty set
{f} is non empty trivial finite 1 -element countable Element of bool the carrier of R
QOE is set
[QOE,f] is V13() non empty set
{QOE,f} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,f},{QOE}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[f,QOE] is V13() non empty set
{f,QOE} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,QOE},{f}} is non empty finite V34() countable set
dom the InternalRel of R is non empty Element of bool the carrier of R
R is Relation-like set
(R) is Relation-like asymmetric set
R ~ is Relation-like set
R \ (R ~) is Relation-like Element of bool R
bool R is non empty set
field R is set
IR is set
CR is set
[IR,CR] is V13() non empty set
{IR,CR} is non empty finite countable set
{IR} is non empty trivial finite 1 -element countable set
{{IR,CR},{IR}} is non empty finite V34() countable set
[CR,IR] is V13() non empty set
{CR,IR} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,IR},{CR}} is non empty finite V34() countable set
R is Relation-like set
(R) is Relation-like asymmetric set
R ~ is Relation-like set
R \ (R ~) is Relation-like Element of bool R
bool R is non empty set
field R is set
IR is set
field (R) is set
CR is set
f is set
[IR,CR] is V13() non empty set
{IR,CR} is non empty finite countable set
{IR} is non empty trivial finite 1 -element countable set
{{IR,CR},{IR}} is non empty finite V34() countable set
[CR,f] is V13() non empty set
{CR,f} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,f},{CR}} is non empty finite V34() countable set
[IR,f] is V13() non empty set
{IR,f} is non empty finite countable set
{{IR,f},{IR}} is non empty finite V34() countable set
[CR,IR] is V13() non empty set
{CR,IR} is non empty finite countable set
{{CR,IR},{CR}} is non empty finite V34() countable set
[f,IR] is V13() non empty set
{f,IR} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,IR},{f}} is non empty finite V34() countable set
R is Relation-like set
(R) is Relation-like asymmetric set
R ~ is Relation-like set
R \ (R ~) is Relation-like Element of bool R
bool R is non empty set
IR is set
CR is set
[IR,CR] is V13() non empty set
{IR,CR} is non empty finite countable set
{IR} is non empty trivial finite 1 -element countable set
{{IR,CR},{IR}} is non empty finite V34() countable set
field R is set
field (R) is set
[CR,IR] is V13() non empty set
{CR,IR} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,IR},{CR}} is non empty finite V34() countable set
R is RelStr
(R) is strict antisymmetric RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is strict RelStr
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is set
[: the carrier of (R), the carrier of (R):] is Relation-like set
bool [: the carrier of (R), the carrier of (R):] is non empty set
S is set
f9 is set
the InternalRel of R -Seg f9 is set
( the InternalRel of R -Seg f9) /\ S is set
n is set
the InternalRel of (R) -Seg n is set
( the InternalRel of (R) -Seg n) /\ S is set
n1 is set
n1 is set
[n1,n] is V13() non empty set
{n1,n} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,n},{n1}} is non empty finite V34() countable set
the InternalRel of R -Seg n is set
R is RelStr
(R) is strict antisymmetric RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is strict RelStr
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is set
[: the carrier of (R), the carrier of (R):] is Relation-like set
bool [: the carrier of (R), the carrier of (R):] is non empty set
QOE is set
S is set
the InternalRel of (R) -Seg S is set
( the InternalRel of (R) -Seg S) /\ QOE is set
f9 is set
the InternalRel of R -Seg f9 is set
( the InternalRel of R -Seg f9) /\ QOE is set
n is set
[n,f9] is V13() non empty set
{n,f9} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,f9},{n}} is non empty finite V34() countable set
[f9,n] is V13() non empty set
{f9,n} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n},{f9}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of (R) -Seg f9 is set
R is RelStr
(R) is strict antisymmetric RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is strict RelStr
the carrier of (R) is set
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
[: the carrier of (R), the carrier of (R):] is Relation-like set
bool [: the carrier of (R), the carrier of (R):] is non empty set
IR is set
CR is Element of the carrier of (R)
S is Element of the carrier of R
[S,CR] is V13() non empty set
{S,CR} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,CR},{S}} is non empty finite V34() countable set
[CR,S] is V13() non empty set
{CR,S} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,S},{CR}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[CR,S] is V13() non empty set
{CR,S} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,S},{CR}} is non empty finite V34() countable set
[CR,S] is V13() non empty set
{CR,S} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,S},{CR}} is non empty finite V34() countable set
[CR,S] is V13() non empty set
{CR,S} is non empty finite countable set
{CR} is non empty trivial finite 1 -element countable set
{{CR,S},{CR}} is non empty finite V34() countable set
S is set
[S,CR] is V13() non empty set
{S,CR} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,CR},{S}} is non empty finite V34() countable set
S is set
[S,CR] is V13() non empty set
{S,CR} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,CR},{S}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
f9 is Element of the carrier of R
[f9,CR] is V13() non empty set
{f9,CR} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,CR},{f9}} is non empty finite V34() countable set
[CR,f9] is V13() non empty set
{CR,f9} is non empty finite countable set
{{CR,f9},{CR}} is non empty finite V34() countable set
R is non empty RelStr
the carrier of R is non empty set
IR is non empty RelStr
the carrier of IR is non empty set
[: the carrier of R, the carrier of IR:] is Relation-like non empty set
bool [: the carrier of R, the carrier of IR:] is non empty set
(IR) is non empty strict antisymmetric RelStr
the InternalRel of IR is Relation-like the carrier of IR -defined the carrier of IR -valued Element of bool [: the carrier of IR, the carrier of IR:]
[: the carrier of IR, the carrier of IR:] is Relation-like non empty set
bool [: the carrier of IR, the carrier of IR:] is non empty set
( the carrier of IR, the InternalRel of IR) is Relation-like the carrier of IR -defined the carrier of IR -valued asymmetric Element of bool [: the carrier of IR, the carrier of IR:]
the InternalRel of IR ~ is Relation-like set
the InternalRel of IR \ ( the InternalRel of IR ~) is Relation-like the carrier of IR -defined the carrier of IR -valued Element of bool the InternalRel of IR
bool the InternalRel of IR is non empty set
RelStr(# the carrier of IR,( the carrier of IR, the InternalRel of IR) #) is non empty strict RelStr
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
(R) is non empty strict antisymmetric RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
CR is Relation-like the carrier of R -defined the carrier of IR -valued Function-like non empty V19( the carrier of R) V20( the carrier of R, the carrier of IR) Element of bool [: the carrier of R, the carrier of IR:]
the carrier of (R) is non empty set
[:NAT, the carrier of (R):] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of (R):] is non empty non trivial non finite set
S is Relation-like NAT -defined the carrier of (R) -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of (R)) Element of bool [:NAT, the carrier of (R):]
S is Relation-like NAT -defined the carrier of (R) -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of (R)) Element of bool [:NAT, the carrier of (R):]
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
f9 is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
[:NAT, the carrier of IR:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of IR:] is non empty non trivial non finite set
n is Relation-like NAT -defined the carrier of IR -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of IR) Element of bool [:NAT, the carrier of IR:]
the carrier of (IR) is non empty set
[:NAT, the carrier of (IR):] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of (IR):] is non empty non trivial non finite set
l is V25() V29() finite cardinal countable ext-real non negative set
l + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
S . (l + 1) is Element of the carrier of (R)
S . l is Element of the carrier of (R)
[(S . (l + 1)),(S . l)] is V13() non empty Element of the carrier of [:(R),(R):]
[:(R),(R):] is non empty strict antisymmetric RelStr
the carrier of [:(R),(R):] is non empty set
{(S . (l + 1)),(S . l)} is non empty finite countable set
{(S . (l + 1))} is non empty trivial finite 1 -element countable set
{{(S . (l + 1)),(S . l)},{(S . (l + 1))}} is non empty finite V34() countable set
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
n1 is Relation-like NAT -defined the carrier of (IR) -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of (IR)) Element of bool [:NAT, the carrier of (IR):]
k is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n1 . k is Element of the carrier of (IR)
S . k is Element of the carrier of (R)
CR . (S . k) is set
n1 . (l + 1) is Element of the carrier of (IR)
n1 . l is Element of the carrier of (IR)
CR . (S . (l + 1)) is set
CR . (S . l) is set
f9 . (l + 1) is Element of the carrier of R
f9 . l is Element of the carrier of R
[(f9 . (l + 1)),(f9 . l)] is V13() non empty Element of the carrier of [:R,R:]
[:R,R:] is non empty strict RelStr
the carrier of [:R,R:] is non empty set
{(f9 . (l + 1)),(f9 . l)} is non empty finite countable set
{(f9 . (l + 1))} is non empty trivial finite 1 -element countable set
{{(f9 . (l + 1)),(f9 . l)},{(f9 . (l + 1))}} is non empty finite V34() countable set
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
a is Element of the carrier of R
b is Element of the carrier of R
n . (l + 1) is Element of the carrier of IR
CR . a is Element of the carrier of IR
n . k is Element of the carrier of IR
CR . b is Element of the carrier of IR
n . l is Element of the carrier of IR
[(n1 . (l + 1)),(n1 . l)] is V13() non empty Element of the carrier of [:(IR),(IR):]
[:(IR),(IR):] is non empty strict antisymmetric RelStr
the carrier of [:(IR),(IR):] is non empty set
{(n1 . (l + 1)),(n1 . l)} is non empty finite countable set
{(n1 . (l + 1))} is non empty trivial finite 1 -element countable set
{{(n1 . (l + 1)),(n1 . l)},{(n1 . (l + 1))}} is non empty finite V34() countable set
[(n1 . l),(n1 . (l + 1))] is V13() non empty Element of the carrier of [:(IR),(IR):]
{(n1 . l),(n1 . (l + 1))} is non empty finite countable set
{(n1 . l)} is non empty trivial finite 1 -element countable set
{{(n1 . l),(n1 . (l + 1))},{(n1 . l)}} is non empty finite V34() countable set
the InternalRel of IR ~ is Relation-like the carrier of IR -defined the carrier of IR -valued Element of bool [: the carrier of IR, the carrier of IR:]
the InternalRel of (IR) is Relation-like the carrier of (IR) -defined the carrier of (IR) -valued Element of bool [: the carrier of (IR), the carrier of (IR):]
[: the carrier of (IR), the carrier of (IR):] is Relation-like non empty set
bool [: the carrier of (IR), the carrier of (IR):] is non empty set
R is non empty RelStr
the carrier of R is non empty set
bool the carrier of R is non empty set
bool (bool the carrier of R) is non empty set
(R) is non empty strict antisymmetric RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
the carrier of (R) is non empty set
IR is Element of bool the carrier of R
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
Class (R) is non empty with_non-empty_elements a_partition of the carrier of R
{ (b1 /\ IR) where b1 is Element of Class (R) : ex b2 being Element of the carrier of (R) st
( b1 = Class ((R),b2) & b2 is_minimal_wrt IR, the InternalRel of (R) ) } is set
QOE is set
bool the carrier of R is non empty Element of bool (bool the carrier of R)
S is Element of Class (R)
S /\ IR is Element of bool the carrier of R
f9 is Element of the carrier of (R)
Class ((R),f9) is Element of bool the carrier of R
QOE is Element of bool (bool the carrier of R)
S is set
f9 is Element of Class (R)
f9 /\ IR is Element of bool the carrier of R
n is Element of the carrier of (R)
Class ((R),n) is Element of bool the carrier of R
f9 is Element of the carrier of (R)
Class ((R),f9) is Element of bool the carrier of R
(Class ((R),f9)) /\ IR is Element of bool the carrier of R
n is Element of the carrier of R
EqClass ((R),n) is Element of Class (R)
f is Element of bool (bool the carrier of R)
QOE is Element of bool (bool the carrier of R)
S is set
f9 is Element of the carrier of (R)
Class ((R),f9) is Element of bool the carrier of R
(Class ((R),f9)) /\ IR is Element of bool the carrier of R
f9 is Element of the carrier of (R)
Class ((R),f9) is Element of bool the carrier of R
(Class ((R),f9)) /\ IR is Element of bool the carrier of R
R is non empty RelStr
the carrier of R is non empty set
bool the carrier of R is non empty set
(R) is non empty strict antisymmetric RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
the carrier of (R) is non empty set
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
IR is Element of bool the carrier of R
(R,IR) is Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
CR is set
f9 is Element of the carrier of (R)
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
n is Element of the carrier of (R)
Class ((R),n) is Element of bool the carrier of R
(Class ((R),n)) /\ IR is Element of bool the carrier of R
[f9,n] is V13() non empty Element of the carrier of [:(R),(R):]
[:(R),(R):] is non empty strict antisymmetric RelStr
the carrier of [:(R),(R):] is non empty set
{f9,n} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n},{f9}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
n1 is set
[n1,f9] is V13() non empty set
{n1,f9} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,f9},{n1}} is non empty finite V34() countable set
n1 is set
[n1,f9] is V13() non empty set
{n1,f9} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,f9},{n1}} is non empty finite V34() countable set
[n1,n] is V13() non empty set
{n1,n} is non empty finite countable set
{{n1,n},{n1}} is non empty finite V34() countable set
[n,n1] is V13() non empty set
{n,n1} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,n1},{n}} is non empty finite V34() countable set
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
R is non empty RelStr
(R) is non empty strict antisymmetric RelStr
the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
bool the carrier of R is non empty set
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is non empty set
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
QOE is Element of bool the carrier of R
bool the carrier of (R) is non empty set
S is Element of bool the carrier of (R)
f9 is set
the InternalRel of (R) -Seg f9 is set
( the InternalRel of (R) -Seg f9) /\ S is Element of bool the carrier of (R)
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
n is Element of the carrier of (R)
Class ((R),n) is Element of bool the carrier of R
(Class ((R),n)) /\ QOE is Element of bool the carrier of R
l is set
[l,n] is V13() non empty set
{l,n} is non empty finite countable set
{l} is non empty trivial finite 1 -element countable set
{{l,n},{l}} is non empty finite V34() countable set
l is set
[l,n] is V13() non empty set
{l,n} is non empty finite countable set
{l} is non empty trivial finite 1 -element countable set
{{l,n},{l}} is non empty finite V34() countable set
the InternalRel of (R) -Seg n is set
(R,QOE) is Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
QOE is set
S is Element of bool the carrier of R
(R,S) is Element of bool (bool the carrier of R)
f9 is set
n is Element of the carrier of (R)
Class ((R),n) is Element of bool the carrier of R
(Class ((R),n)) /\ S is Element of bool the carrier of R
n1 is set
l is set
the InternalRel of (R) -Seg l is set
( the InternalRel of (R) -Seg l) /\ QOE is set
k is set
a is Element of the carrier of (R)
[a,n] is V13() non empty Element of the carrier of [:(R),(R):]
[:(R),(R):] is non empty strict antisymmetric RelStr
the carrier of [:(R),(R):] is non empty set
{a,n} is non empty finite countable set
{a} is non empty trivial finite 1 -element countable set
{{a,n},{a}} is non empty finite V34() countable set
R is non empty RelStr
the carrier of R is non empty set
bool the carrier of R is non empty set
(R) is non empty strict antisymmetric RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
the carrier of (R) is non empty set
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
IR is Element of bool the carrier of R
(R,IR) is Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
CR is Element of the carrier of (R)
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
Class ((R),CR) is Element of bool the carrier of R
(Class ((R),CR)) /\ IR is Element of bool the carrier of R
f is set
R is non empty RelStr
the carrier of R is non empty set
bool the carrier of R is non empty set
IR is Element of bool the carrier of R
(R,IR) is Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
CR is set
(R) is non empty strict antisymmetric RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
the carrier of (R) is non empty set
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
f is Element of the carrier of (R)
Class ((R),f) is Element of bool the carrier of R
(Class ((R),f)) /\ IR is Element of bool the carrier of R
R is non empty RelStr
(R) is non empty strict antisymmetric RelStr
the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
bool the carrier of R is non empty set
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is non empty set
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
QOE is non empty Element of bool the carrier of R
(R,QOE) is Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
S is set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
f9 is Element of the carrier of (R)
Class ((R),f9) is Element of bool the carrier of R
(Class ((R),f9)) /\ QOE is Element of bool the carrier of R
n is set
n1 is Element of the carrier of (R)
Class ((R),n1) is Element of bool the carrier of R
(Class ((R),n1)) /\ QOE is Element of bool the carrier of R
l is Element of the carrier of R
k is Element of the carrier of R
[f9,n1] is V13() non empty Element of the carrier of [:(R),(R):]
[:(R),(R):] is non empty strict antisymmetric RelStr
the carrier of [:(R),(R):] is non empty set
{f9,n1} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
[n1,f9] is V13() non empty Element of the carrier of [:(R),(R):]
{n1,f9} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,f9},{n1}} is non empty finite V34() countable set
[n1,f9] is V13() non empty Element of the carrier of [:(R),(R):]
{n1,f9} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,f9},{n1}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[n1,f9] is V13() non empty Element of the carrier of [:(R),(R):]
{n1,f9} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,f9},{n1}} is non empty finite V34() countable set
[n1,f9] is V13() non empty Element of the carrier of [:(R),(R):]
{n1,f9} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,f9},{n1}} is non empty finite V34() countable set
k is Element of the carrier of R
l is Element of the carrier of R
[n1,f9] is V13() non empty Element of the carrier of [:(R),(R):]
[:(R),(R):] is non empty strict antisymmetric RelStr
the carrier of [:(R),(R):] is non empty set
{n1,f9} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,f9},{n1}} is non empty finite V34() countable set
[f9,n1] is V13() non empty Element of the carrier of [:(R),(R):]
{f9,n1} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
[f9,n1] is V13() non empty Element of the carrier of [:(R),(R):]
{f9,n1} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[f9,n1] is V13() non empty Element of the carrier of [:(R),(R):]
{f9,n1} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
[f9,n1] is V13() non empty Element of the carrier of [:(R),(R):]
{f9,n1} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
l is Element of the carrier of R
k is Element of the carrier of R
[f9,n1] is V13() non empty Element of the carrier of [:(R),(R):]
[:(R),(R):] is non empty strict antisymmetric RelStr
the carrier of [:(R),(R):] is non empty set
{f9,n1} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
[n1,f9] is V13() non empty Element of the carrier of [:(R),(R):]
{n1,f9} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,f9},{n1}} is non empty finite V34() countable set
[f9,n1] is V13() non empty Element of the carrier of [:(R),(R):]
[:(R),(R):] is non empty strict antisymmetric RelStr
the carrier of [:(R),(R):] is non empty set
{f9,n1} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
[n1,f9] is V13() non empty Element of the carrier of [:(R),(R):]
{n1,f9} is non empty finite countable set
{n1} is non empty trivial finite 1 -element countable set
{{n1,f9},{n1}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
{S} is non empty trivial finite 1 -element countable set
card (R,QOE) is V25() cardinal set
QOE is Element of the carrier of R
S is Element of the carrier of R
[QOE,S] is V13() non empty Element of the carrier of [:R,R:]
[:R,R:] is non empty strict RelStr
the carrier of [:R,R:] is non empty set
{QOE,S} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,S},{QOE}} is non empty finite V34() countable set
[S,QOE] is V13() non empty Element of the carrier of [:R,R:]
{S,QOE} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,QOE},{S}} is non empty finite V34() countable set
{QOE,S} is non empty finite countable Element of bool the carrier of R
{QOE} is non empty trivial finite 1 -element countable Element of bool the carrier of R
{S} is non empty trivial finite 1 -element countable Element of bool the carrier of R
{{QOE},{S}} is non empty finite V34() countable Element of bool (bool the carrier of R)
n1 is set
(R,{QOE,S}) is Element of bool (bool the carrier of R)
l is Element of the carrier of (R)
Class ((R),l) is Element of bool the carrier of R
(Class ((R),l)) /\ {QOE,S} is finite countable Element of bool the carrier of R
k is set
Class ((R),QOE) is Element of bool the carrier of R
k is set
Class ((R),S) is Element of bool the carrier of R
l is Element of the carrier of (R)
k is Element of the carrier of (R)
a is set
[a,k] is V13() non empty set
{a,k} is non empty finite countable set
{a} is non empty trivial finite 1 -element countable set
{{a,k},{a}} is non empty finite V34() countable set
a is set
[a,k] is V13() non empty set
{a,k} is non empty finite countable set
{a} is non empty trivial finite 1 -element countable set
{{a,k},{a}} is non empty finite V34() countable set
a is set
Class ((R),QOE) is Element of bool the carrier of R
(Class ((R),QOE)) /\ {QOE,S} is finite countable Element of bool the carrier of R
Class ((R),k) is Element of bool the carrier of R
(Class ((R),k)) /\ {QOE,S} is finite countable Element of bool the carrier of R
l is Element of the carrier of (R)
Class ((R),l) is Element of bool the carrier of R
(Class ((R),l)) /\ {QOE,S} is finite countable Element of bool the carrier of R
l is Element of the carrier of (R)
k is Element of the carrier of (R)
a is set
[a,k] is V13() non empty set
{a,k} is non empty finite countable set
{a} is non empty trivial finite 1 -element countable set
{{a,k},{a}} is non empty finite V34() countable set
a is set
[a,k] is V13() non empty set
{a,k} is non empty finite countable set
{a} is non empty trivial finite 1 -element countable set
{{a,k},{a}} is non empty finite V34() countable set
a is set
Class ((R),S) is Element of bool the carrier of R
(Class ((R),S)) /\ {QOE,S} is finite countable Element of bool the carrier of R
Class ((R),k) is Element of bool the carrier of R
(Class ((R),k)) /\ {QOE,S} is finite countable Element of bool the carrier of R
l is Element of the carrier of (R)
Class ((R),l) is Element of bool the carrier of R
(Class ((R),l)) /\ {QOE,S} is finite countable Element of bool the carrier of R
card {{QOE},{S}} is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
QOE is Element of bool the carrier of R
(R,QOE) is Element of bool (bool the carrier of R)
card (R,QOE) is V25() cardinal set
R is non empty V81() reflexive transitive antisymmetric non void RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued non empty V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive antisymmetric transitive Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is non empty set
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
bool the carrier of R is non empty set
(R) is non empty strict transitive antisymmetric RelStr
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
f is non empty Element of bool the carrier of R
(R,f) is Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
card (R,f) is V25() cardinal set
R is RelStr
the carrier of R is set
bool the carrier of R is non empty set
R is RelStr
the carrier of R is set
{} the carrier of R is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() strongly_connected ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() Element of bool the carrier of R
bool the carrier of R is non empty set
CR is Element of the carrier of R
R is non empty RelStr
the carrier of R is non empty set
bool the carrier of R is non empty set
IR is non empty Element of bool the carrier of R
CR is set
the Element of IR is Element of IR
QOE is Element of the carrier of R
R is non empty RelStr
(R) is non empty strict antisymmetric RelStr
the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is non empty set
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
bool the carrier of R is non empty set
S is Element of bool the carrier of R
{} the carrier of R is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial proper V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() strongly_connected ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() Element of bool the carrier of R
f9 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
{} the carrier of R is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial proper V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() strongly_connected ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() Element of bool the carrier of R
f9 is set
the InternalRel of (R) -Seg f9 is set
( the InternalRel of (R) -Seg f9) /\ S is Element of bool the carrier of R
{f9} is non empty trivial finite 1 -element countable set
n is non empty trivial finite 1 -element countable set
n1 is Element of S
{n1} is non empty trivial finite 1 -element countable set
bool S is non empty set
l is Element of the carrier of R
k is Element of the carrier of R
[l,k] is V13() non empty Element of the carrier of [:R,R:]
[:R,R:] is non empty strict RelStr
the carrier of [:R,R:] is non empty set
{l,k} is non empty finite countable set
{l} is non empty trivial finite 1 -element countable set
{{l,k},{l}} is non empty finite V34() countable set
the InternalRel of (R) -Seg k is set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[k,l] is V13() non empty Element of the carrier of [:R,R:]
{k,l} is non empty finite countable set
{k} is non empty trivial finite 1 -element countable set
{{k,l},{k}} is non empty finite V34() countable set
{} the carrier of R is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial proper V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() strongly_connected ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() Element of bool the carrier of R
R is RelStr
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
IR is RelStr
the InternalRel of IR is Relation-like the carrier of IR -defined the carrier of IR -valued Element of bool [: the carrier of IR, the carrier of IR:]
the carrier of IR is set
[: the carrier of IR, the carrier of IR:] is Relation-like set
bool [: the carrier of IR, the carrier of IR:] is non empty set
bool the carrier of IR is non empty set
CR is Element of bool the carrier of IR
bool the carrier of R is non empty set
f is Element of bool the carrier of R
QOE is set
S is Element of the carrier of IR
f9 is Element of the carrier of R
n is Element of the carrier of R
n1 is Element of the carrier of IR
[n,f9] is V13() non empty set
{n,f9} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,f9},{n}} is non empty finite V34() countable set
l is Element of the carrier of IR
R is Relation-like Function-like set
dom R is set
IR is set
rng R is set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : R . b1 = IR } is set
f is set
R . f is set
QOE is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
S is set
f9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
R . f9 is set
S is non empty countable V267() V268() V269() V270() V271() V272() V281() V283() Element of bool NAT
min S is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
R . f9 is set
n is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
R . n is set
n is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
R . n is set
CR is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
R . CR is set
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
R . f is set
R is non empty 1-sorted
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
CR is set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( not b1 <= f & IR . b1 = CR ) } is set
S is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . S is Element of the carrier of R
S is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . S is Element of the carrier of R
f9 is set
n is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . n is Element of the carrier of R
f9 is non empty countable V267() V268() V269() V270() V271() V272() V281() V283() Element of bool NAT
min f9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . n is Element of the carrier of R
n1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . n1 is Element of the carrier of R
n1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . n1 is Element of the carrier of R
QOE is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . QOE is Element of the carrier of R
S is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . S is Element of the carrier of R
R is non empty RelStr
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
IR is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
rng IR is non empty Element of bool the carrier of R
bool the carrier of R is non empty set
dom IR is non empty countable V267() V268() V269() V270() V271() V272() V281() V283() Element of bool NAT
f is set
QOE is non empty finite countable set
{ H1(b1) where b1 is Element of QOE : S1[b1] } is set
the Element of QOE is Element of QOE
(IR, the Element of QOE) is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n is set
n1 is Element of QOE
(IR,n1) is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n is non empty finite countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of bool NAT
sup n is V25() V29() finite cardinal countable V251() ext-real non negative V255() V256() set
n1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n1 + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
IR . (n1 + 1) is Element of the carrier of R
k is Element of the carrier of R
a is Element of the carrier of R
(IR,a) is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
b is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . b is Element of the carrier of R
R is RelStr
the carrier of R is set
bool the carrier of R is non empty set
(R) is strict antisymmetric RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is strict RelStr
the carrier of (R) is set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
[: the carrier of (R), the carrier of (R):] is Relation-like set
bool [: the carrier of (R), the carrier of (R):] is non empty set
IR is Element of bool the carrier of R
CR is Element of the carrier of (R)
the InternalRel of R -Seg CR is set
( the InternalRel of R -Seg CR) /\ IR is Element of bool the carrier of R
Class ((R),CR) is Element of bool the carrier of R
S is set
[S,CR] is V13() non empty set
{S,CR} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,CR},{S}} is non empty finite V34() countable set
S is set
[S,CR] is V13() non empty set
{S,CR} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,CR},{S}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
R is non empty RelStr
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
bool the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
(R) is non empty strict antisymmetric RelStr
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is non empty set
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
f is non empty Element of bool the carrier of R
(R,f) is Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
[:NAT,(R,f):] is Relation-like set
bool [:NAT,(R,f):] is non empty set
S is Relation-like NAT -defined (R,f) -valued Function-like V20( NAT ,(R,f)) Element of bool [:NAT,(R,f):]
f9 is set
n is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
S . n is Element of (R,f)
S . f9 is set
QOE is non empty non trivial non finite set
choose (S . n) is Element of S . n
choose (S . f9) is Element of S . f9
f9 is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
n is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
l is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n . n1 is Element of the carrier of R
n . l is Element of the carrier of R
k is Element of the carrier of (R)
a is Element of the carrier of (R)
[k,a] is V13() non empty Element of the carrier of [:(R),(R):]
[:(R),(R):] is non empty strict antisymmetric RelStr
the carrier of [:(R),(R):] is non empty set
{k,a} is non empty finite countable set
{k} is non empty trivial finite 1 -element countable set
{{k,a},{k}} is non empty finite V34() countable set
S . n1 is Element of (R,f)
S . l is Element of (R,f)
choose (S . l) is Element of S . l
choose (S . n1) is Element of S . n1
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
Class ((R),a) is Element of bool the carrier of R
Class ((R),k) is Element of bool the carrier of R
b is Element of the carrier of (R)
Class ((R),b) is Element of bool the carrier of R
(Class ((R),b)) /\ f is Element of bool the carrier of R
S is Element of the carrier of (R)
Class ((R),S) is Element of bool the carrier of R
(Class ((R),S)) /\ f is Element of bool the carrier of R
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
choose f is Element of f
QOE is Relation-like Function-like set
dom QOE is set
QOE . 0 is set
S is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
QOE . S is set
f9 is Element of the carrier of (R)
the InternalRel of R -Seg f9 is set
( the InternalRel of R -Seg f9) /\ f is Element of bool the carrier of R
Class ((R),f9) is Element of bool the carrier of R
(( the InternalRel of R -Seg f9) /\ f) \ (Class ((R),f9)) is Element of bool the carrier of R
S + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
QOE . (S + 1) is set
the InternalRel of R -Seg (QOE . S) is set
( the InternalRel of R -Seg (QOE . S)) /\ f is Element of bool the carrier of R
Class ((R),(QOE . S)) is Element of bool the carrier of R
(( the InternalRel of R -Seg (QOE . S)) /\ f) \ (Class ((R),(QOE . S))) is Element of bool the carrier of R
choose ((( the InternalRel of R -Seg (QOE . S)) /\ f) \ (Class ((R),(QOE . S)))) is Element of (( the InternalRel of R -Seg (QOE . S)) /\ f) \ (Class ((R),(QOE . S)))
S is set
QOE . S is set
f9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
S is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
S . f9 is Element of the carrier of R
S . 0 is Element of the carrier of R
n is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
S . n is Element of the carrier of R
n + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
S . (n + 1) is Element of the carrier of R
n1 is Element of the carrier of (R)
the InternalRel of R -Seg n1 is set
( the InternalRel of R -Seg n1) /\ f is Element of bool the carrier of R
Class ((R),n1) is Element of bool the carrier of R
(( the InternalRel of R -Seg n1) /\ f) \ (Class ((R),n1)) is Element of bool the carrier of R
l is Element of the carrier of (R)
choose ((( the InternalRel of R -Seg n1) /\ f) \ (Class ((R),n1))) is Element of (( the InternalRel of R -Seg n1) /\ f) \ (Class ((R),n1))
[l,n1] is V13() non empty Element of the carrier of [:(R),(R):]
[:(R),(R):] is non empty strict antisymmetric RelStr
the carrier of [:(R),(R):] is non empty set
{l,n1} is non empty finite countable set
{l} is non empty trivial finite 1 -element countable set
{{l,n1},{l}} is non empty finite V34() countable set
f9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
S . f9 is Element of the carrier of R
n is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
S . n is Element of the carrier of R
n + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
S . (n + 1) is Element of the carrier of R
n1 is Element of the carrier of (R)
l is Element of the carrier of (R)
Class ((R),n1) is Element of bool the carrier of R
the InternalRel of R -Seg n1 is set
( the InternalRel of R -Seg n1) /\ f is Element of bool the carrier of R
(( the InternalRel of R -Seg n1) /\ f) \ (Class ((R),n1)) is Element of bool the carrier of R
choose ((( the InternalRel of R -Seg n1) /\ f) \ (Class ((R),n1))) is Element of (( the InternalRel of R -Seg n1) /\ f) \ (Class ((R),n1))
l is Element of the carrier of (R)
Class ((R),n1) is Element of bool the carrier of R
the InternalRel of R -Seg n1 is set
( the InternalRel of R -Seg n1) /\ f is Element of bool the carrier of R
(( the InternalRel of R -Seg n1) /\ f) \ (Class ((R),n1)) is Element of bool the carrier of R
choose ((( the InternalRel of R -Seg n1) /\ f) \ (Class ((R),n1))) is Element of (( the InternalRel of R -Seg n1) /\ f) \ (Class ((R),n1))
R is non empty RelStr
the carrier of R is non empty set
bool the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
(R) is non empty strict antisymmetric RelStr
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is non empty set
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
QOE is Element of bool the carrier of R
{} the carrier of R is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial proper V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() strongly_connected ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() Element of bool the carrier of R
S is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
bool (bool the carrier of R) is non empty set
S is non empty Element of bool the carrier of R
(R,S) is Element of bool (bool the carrier of R)
f9 is non empty finite countable Element of bool (bool the carrier of R)
{ (choose b1) where b1 is Element of f9 : verum } is set
n is set
n1 is set
l is Element of f9
choose l is Element of l
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
k is Element of the carrier of (R)
Class ((R),k) is Element of bool the carrier of R
(Class ((R),k)) /\ QOE is Element of bool the carrier of R
n1 is Element of the carrier of R
{ b1 where b1 is Element of S : S1[b1] } is set
bool S is non empty set
k is non empty Element of bool the carrier of R
(R,k) is Element of bool (bool the carrier of R)
the Element of (R,k) is Element of (R,k)
b is non empty set
the Element of b is Element of b
CP9 is Element of the carrier of (R)
Class ((R),CP9) is Element of bool the carrier of R
(Class ((R),CP9)) /\ k is Element of bool the carrier of R
f is Element of the carrier of (R)
f9 is Element of S
f9 is set
[f9,f] is V13() non empty set
{f9,f} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,f},{f9}} is non empty finite V34() countable set
f is Element of the carrier of R
f is Element of the carrier of R
x is Element of S
Class ((R),f) is Element of bool the carrier of R
(Class ((R),f)) /\ QOE is Element of bool the carrier of R
(R,QOE) is Element of bool (bool the carrier of R)
choose ((Class ((R),f)) /\ QOE) is Element of (Class ((R),f)) /\ QOE
f is Element of the carrier of R
[f,f] is V13() non empty Element of the carrier of [:R,(R):]
[:R,(R):] is non empty strict RelStr
the carrier of [:R,(R):] is non empty set
{f,f} is non empty finite countable set
{f} is non empty trivial finite 1 -element countable set
{{f,f},{f}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R /\ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
x is Element of S
{ H1(b1) where b1 is Element of f9 : S1[b1] } is set
{} the carrier of R is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial proper V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() strongly_connected ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() Element of bool the carrier of R
R is non empty RelStr
(R) is non empty strict antisymmetric RelStr
the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
IR is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
bool the carrier of R is non empty set
IR is Element of bool the carrier of R
(R,IR) is Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
R is non empty V81() reflexive transitive antisymmetric non void RelStr
the carrier of R is non empty set
bool the carrier of R is non empty set
IR is non empty Element of bool the carrier of R
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued non empty V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive antisymmetric transitive Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
(R) is non empty strict transitive antisymmetric RelStr
( the carrier of R, the InternalRel of R) is Relation-like the carrier of R -defined the carrier of R -valued asymmetric Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R ~ is Relation-like set
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool the InternalRel of R
bool the InternalRel of R is non empty set
RelStr(# the carrier of R,( the carrier of R, the InternalRel of R) #) is non empty strict RelStr
the InternalRel of (R) is Relation-like the carrier of (R) -defined the carrier of (R) -valued Element of bool [: the carrier of (R), the carrier of (R):]
the carrier of (R) is non empty set
[: the carrier of (R), the carrier of (R):] is Relation-like non empty set
bool [: the carrier of (R), the carrier of (R):] is non empty set
{ b1 where b1 is Element of the carrier of (R) : b1 is_minimal_wrt IR, the InternalRel of (R) } is set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
f9 is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
(R,IR) is Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
f9 is set
(R) is Relation-like the carrier of R -defined the carrier of R -valued V19( the carrier of R) V20( the carrier of R, the carrier of R) reflexive symmetric transitive Element of bool [: the carrier of R, the carrier of R:]
n is Element of the carrier of (R)
Class ((R),n) is Element of bool the carrier of R
(Class ((R),n)) /\ IR is Element of bool the carrier of R
n1 is non empty set
l is set
k is Element of the carrier of (R)
l is Element of the carrier of R
the InternalRel of (R) -Seg l is set
( the InternalRel of (R) -Seg l) /\ IR is Element of bool the carrier of R
k is Element of the carrier of (R)
the InternalRel of (R) -Seg l is set
( the InternalRel of (R) -Seg l) /\ IR is Element of bool the carrier of R
a is set
the InternalRel of (R) -Seg a is set
[a,l] is V13() non empty set
{a,l} is non empty finite countable set
{a} is non empty trivial finite 1 -element countable set
{{a,l},{a}} is non empty finite V34() countable set
dom the InternalRel of (R) is Element of bool the carrier of (R)
bool the carrier of (R) is non empty set
b is Element of the carrier of (R)
k is Element of the carrier of (R)
the InternalRel of (R) -Seg k is set
( the InternalRel of (R) -Seg k) /\ IR is Element of bool the carrier of R
[b,l] is V13() non empty Element of the carrier of [:(R),R:]
[:(R),R:] is non empty strict transitive antisymmetric RelStr
the carrier of [:(R),R:] is non empty set
{b,l} is non empty finite countable set
{b} is non empty trivial finite 1 -element countable set
{{b,l},{b}} is non empty finite V34() countable set
the InternalRel of R ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of R \ ( the InternalRel of R ~) is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
S is Element of the carrier of R
the InternalRel of (R) -Seg l is set
( the InternalRel of (R) -Seg l) /\ IR is Element of bool the carrier of R
a is Element of the carrier of R
l is set
k is set
a is Element of the carrier of R
b is Element of the carrier of R
[b,k] is V13() non empty set
{b,k} is non empty finite countable set
{b} is non empty trivial finite 1 -element countable set
{{b,k},{b}} is non empty finite V34() countable set
[k,b] is V13() non empty set
{k,b} is non empty finite countable set
{k} is non empty trivial finite 1 -element countable set
{{k,b},{k}} is non empty finite V34() countable set
S is Element of the carrier of (R)
R is non empty RelStr
the carrier of R is non empty set
bool the carrier of R is non empty set
bool (bool the carrier of R) is non empty set
IR is Element of bool the carrier of R
bool IR is non empty set
{ b1 where b1 is Element of bool IR : (R,IR,b1) } is set
QOE is set
S is set
f9 is Element of bool IR
bool the carrier of R is non empty Element of bool (bool the carrier of R)
S is non empty Element of bool (bool the carrier of R)
f9 is set
n is Element of bool IR
CR is non empty Element of bool (bool the carrier of R)
f is non empty Element of bool (bool the carrier of R)
QOE is set
R is non empty RelStr
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
IR is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
rng IR is non empty Element of bool the carrier of R
bool the carrier of R is non empty set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( a1 <= IR . b1 & not b1 <= a2 ) } is set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : a1 <= IR . b1 } is set
{ (IR . b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . a2 <= IR . b1 & not b1 <= a2 ) } is set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . a2 <= IR . b1 & not b1 <= a2 ) } is set
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
QOE is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . QOE is Element of the carrier of R
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . QOE <= IR . b1 & not b1 <= QOE ) } is set
{ (IR . b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . QOE <= IR . b1 & not b1 <= QOE ) } is set
f9 is set
n is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . n is Element of the carrier of R
f9 is Element of bool the carrier of R
n1 is set
l is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . l is Element of the carrier of R
f9 is Element of bool the carrier of R
(R,f9) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
{ b1 where b1 is Element of (R,f9) : b1 is finite } is set
choose { b1 where b1 is Element of (R,f9) : b1 is finite } is Element of { b1 where b1 is Element of (R,f9) : b1 is finite }
k is set
a is Element of (R,f9)
a is non empty Element of bool the carrier of R
{ b1 where b1 is Element of a : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,QOE) is finite ) } is set
choose { b1 where b1 is Element of a : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,QOE) is finite ) } is Element of { b1 where b1 is Element of a : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,QOE) is finite ) }
(R,IR,(choose { b1 where b1 is Element of a : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,QOE) is finite ) } ),QOE) is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
CP9 is non empty Element of bool the carrier of R
{ b1 where b1 is Element of CP9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,QOE) is finite ) } is set
choose { b1 where b1 is Element of CP9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,QOE) is finite ) } is Element of { b1 where b1 is Element of CP9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,QOE) is finite ) }
(R,IR,(choose { b1 where b1 is Element of CP9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,QOE) is finite ) } ),QOE) is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f9 is Element of bool the carrier of R
f is set
QOE is non empty set
{ b1 where b1 is Element of QOE : ex b2 being Element of rng IR st
( b2 = b1 & not H2(b2) is finite ) } is set
choose { b1 where b1 is Element of QOE : ex b2 being Element of rng IR st
( b2 = b1 & not H2(b2) is finite ) } is Element of { b1 where b1 is Element of QOE : ex b2 being Element of rng IR st
( b2 = b1 & not H2(b2) is finite ) }
(IR,(choose { b1 where b1 is Element of QOE : ex b2 being Element of rng IR st
( b2 = b1 & not H2(b2) is finite ) } )) is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n is Relation-like NAT -defined NAT -valued Function-like non empty V19( NAT ) V20( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
n . 0 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
dom n is non empty countable V267() V268() V269() V270() V271() V272() V281() V283() Element of bool NAT
rng n is non empty countable V267() V268() V269() V270() V271() V272() V281() V283() Element of bool NAT
{ H2(b1) where b1 is Element of rng IR : b1 in QOE } is set
l is set
k is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : k <= IR . b1 } is set
union { H2(b1) where b1 is Element of rng IR : b1 in QOE } is set
l is set
dom IR is non empty countable V267() V268() V269() V270() V271() V272() V281() V283() Element of bool NAT
k is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . l is set
a is Element of the carrier of R
b is Element of the carrier of R
S is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : S <= IR . b1 } is set
n1 is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : n1 <= IR . b1 } is set
n1 is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : n1 <= IR . b1 } is set
IR . (n . 0) is Element of the carrier of R
l is Element of QOE
k is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : k <= IR . b1 } is set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : IR . (n . 0) <= IR . b1 } is set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (n . 0) <= IR . b1 & not b1 <= n . 0 ) } is set
{ H3(b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( 0 <= b1 & b1 <= n . 0 & S3[b1] ) } is set
b is set
S is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . S is Element of the carrier of R
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (n . 0) <= IR . b1 & not b1 <= n . 0 ) } \/ { H3(b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( 0 <= b1 & b1 <= n . 0 & S3[b1] ) } is set
S is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . S is Element of the carrier of R
{ b2 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : IR . (n . 0) <= IR . b2 } is set
S is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . S is Element of the carrier of R
{ b2 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : IR . (n . 0) <= IR . b2 } is set
{ b2 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : IR . (n . 0) <= IR . b2 } is set
b is Element of QOE
S is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : S <= IR . b1 } is set
{ (IR . b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (n . a1) <= IR . b1 & not b1 <= n . a1 ) } is set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (n . a1) <= IR . b1 & not b1 <= n . a1 ) } is set
0 + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
n . (0 + 1) is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
{ (IR . b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (n . 0) <= IR . b1 & not b1 <= n . 0 ) } is set
b is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n . b is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
b + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
n . (b + 1) is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . (n . b) is Element of the carrier of R
{ (IR . b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (n . b) <= IR . b1 & not b1 <= n . b ) } is set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (n . b) <= IR . b1 & not b1 <= n . b ) } is set
S is Element of bool the carrier of R
CP9 is non empty Element of bool the carrier of R
(R,S) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
{ b1 where b1 is Element of (R,S) : b1 is finite } is set
choose { b1 where b1 is Element of (R,S) : b1 is finite } is Element of { b1 where b1 is Element of (R,S) : b1 is finite }
{ b1 where b1 is Element of CP9 : ex b2 being Element of rng IR st
( b2 = b1 & not { b3 where b3 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( b2 <= IR . b3 & not b3 <= n . b ) } is finite ) } is set
choose { b1 where b1 is Element of CP9 : ex b2 being Element of rng IR st
( b2 = b1 & not { b3 where b3 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( b2 <= IR . b3 & not b3 <= n . b ) } is finite ) } is Element of { b1 where b1 is Element of CP9 : ex b2 being Element of rng IR st
( b2 = b1 & not { b3 where b3 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( b2 <= IR . b3 & not b3 <= n . b ) } is finite ) }
(R,IR,(choose { b1 where b1 is Element of CP9 : ex b2 being Element of rng IR st
( b2 = b1 & not { b3 where b3 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( b2 <= IR . b3 & not b3 <= n . b ) } is finite ) } ),(n . b)) is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
S is Element of bool the carrier of R
CP9 is non empty Element of bool the carrier of R
(R,S) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
{ b1 where b1 is Element of (R,S) : b1 is finite } is set
choose { b1 where b1 is Element of (R,S) : b1 is finite } is Element of { b1 where b1 is Element of (R,S) : b1 is finite }
{ b1 where b1 is Element of CP9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,n . b) is finite ) } is set
choose { b1 where b1 is Element of CP9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,n . b) is finite ) } is Element of { b1 where b1 is Element of CP9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,n . b) is finite ) }
(R,IR,(choose { b1 where b1 is Element of CP9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,n . b) is finite ) } ),(n . b)) is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f is set
x is Element of (R,S)
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( a1 <= IR . b1 & not b1 <= n . b ) } is set
x is Element of (R,S)
{ H4(b1) where b1 is Element of rng IR : b1 in CP9 } is set
y is set
xa is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( xa <= IR . b1 & not b1 <= n . b ) } is set
union { H4(b1) where b1 is Element of rng IR : b1 in CP9 } is set
y is set
xa is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . xa is Element of the carrier of R
xb is Element of the carrier of R
ya is Element of the carrier of R
yb is set
xa9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . xa9 is Element of the carrier of R
yb is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( yb <= IR . b1 & not b1 <= n . b ) } is set
x is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( x <= IR . b1 & not b1 <= n . b ) } is set
x is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( x <= IR . b1 & not b1 <= n . b ) } is set
y is Element of CP9
IR . (n . (b + 1)) is Element of the carrier of R
xa is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . xa is Element of the carrier of R
xa is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . xa is Element of the carrier of R
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (n . (b + 1)) <= IR . b1 & not b1 <= n . b ) } is set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (n . (b + 1)) <= IR . b1 & not b1 <= n . (b + 1) ) } is set
{ H4(b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( not b1 <= n . b & b1 <= n . (b + 1) & S5[b1] ) } is set
yb is set
xa9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . xa9 is Element of the carrier of R
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (n . (b + 1)) <= IR . b1 & not b1 <= n . (b + 1) ) } \/ { H4(b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( not b1 <= n . b & b1 <= n . (b + 1) & S5[b1] ) } is set
xa9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . xa9 is Element of the carrier of R
{ b2 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (n . (b + 1)) <= IR . b2 & not b2 <= n . b ) } is set
xa9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . xa9 is Element of the carrier of R
{ b2 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (n . (b + 1)) <= IR . b2 & not b2 <= n . b ) } is set
{ b2 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (n . (b + 1)) <= IR . b2 & not b2 <= n . b ) } is set
yb is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( yb <= IR . b1 & not b1 <= n . b ) } is set
(b + 1) + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
n . ((b + 1) + 1) is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
{ (IR . b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (n . (b + 1)) <= IR . b1 & not b1 <= n . (b + 1) ) } is set
IR * n is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
S is Relation-like NAT -defined REAL -valued Function-like V20( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
CP9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
S . CP9 is V250() V251() ext-real Element of REAL
rng S is V267() V268() V269() Element of bool REAL
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . f is Element of the carrier of R
{ (IR . b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . f <= IR . b1 & not b1 <= f ) } is set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . f <= IR . b1 & not b1 <= f ) } is set
CP9 + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
S . (CP9 + 1) is V250() V251() ext-real Element of REAL
f is Element of bool the carrier of R
f9 is non empty Element of bool the carrier of R
(R,f) is non empty Element of bool (bool the carrier of R)
{ b1 where b1 is Element of (R,f) : b1 is finite } is set
choose { b1 where b1 is Element of (R,f) : b1 is finite } is Element of { b1 where b1 is Element of (R,f) : b1 is finite }
{ b1 where b1 is Element of f9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,f) is finite ) } is set
choose { b1 where b1 is Element of f9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,f) is finite ) } is Element of { b1 where b1 is Element of f9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,f) is finite ) }
(R,IR,(choose { b1 where b1 is Element of f9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,f) is finite ) } ),f) is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
xa is set
xb is Element of (R,f)
xb is Element of (R,f)
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( a1 <= IR . b1 & not b1 <= f ) } is set
{ H4(b1) where b1 is Element of rng IR : b1 in f9 } is set
yb is set
xa9 is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( xa9 <= IR . b1 & not b1 <= f ) } is set
union { H4(b1) where b1 is Element of rng IR : b1 in f9 } is set
yb is set
xa9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . xa9 is Element of the carrier of R
ya9 is Element of the carrier of R
f1 is Element of the carrier of R
g1 is set
Rn is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . Rn is Element of the carrier of R
g1 is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( g1 <= IR . b1 & not b1 <= f ) } is set
xb is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( xb <= IR . b1 & not b1 <= f ) } is set
xb is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( xb <= IR . b1 & not b1 <= f ) } is set
ya is Element of f9
yb is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( yb <= IR . b1 & not b1 <= f ) } is set
ya is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . ya is Element of the carrier of R
CP9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
S . CP9 is V250() V251() ext-real Element of REAL
CP9 is Relation-like NAT -defined NAT -valued Function-like non empty V19( NAT ) V20( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]
IR * CP9 is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) subsequence of IR
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
(IR * n) . f is Element of the carrier of R
f + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
(IR * n) . (f + 1) is Element of the carrier of R
[((IR * n) . f),((IR * n) . (f + 1))] is V13() non empty set
{((IR * n) . f),((IR * n) . (f + 1))} is non empty finite countable set
{((IR * n) . f)} is non empty trivial finite 1 -element countable set
{{((IR * n) . f),((IR * n) . (f + 1))},{((IR * n) . f)}} is non empty finite V34() countable set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
CP9 . f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . (CP9 . f) is Element of the carrier of R
CP9 . (f + 1) is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . (CP9 . (f + 1)) is Element of the carrier of R
{ (IR . b1) where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (CP9 . f) <= IR . b1 & not b1 <= CP9 . f ) } is set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( IR . (CP9 . f) <= IR . b1 & not b1 <= CP9 . f ) } is set
f is Element of bool the carrier of R
f9 is non empty Element of bool the carrier of R
(R,f) is non empty Element of bool (bool the carrier of R)
{ b1 where b1 is Element of (R,f) : b1 is finite } is set
choose { b1 where b1 is Element of (R,f) : b1 is finite } is Element of { b1 where b1 is Element of (R,f) : b1 is finite }
{ b1 where b1 is Element of f9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,CP9 . f) is finite ) } is set
choose { b1 where b1 is Element of f9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,CP9 . f) is finite ) } is Element of { b1 where b1 is Element of f9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,CP9 . f) is finite ) }
(R,IR,(choose { b1 where b1 is Element of f9 : ex b2 being Element of rng IR st
( b2 = b1 & not H1(b2,CP9 . f) is finite ) } ),(CP9 . f)) is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
xa is set
xb is Element of (R,f)
xb is Element of (R,f)
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( a1 <= IR . b1 & not b1 <= CP9 . f ) } is set
{ H4(b1) where b1 is Element of rng IR : b1 in f9 } is set
yb is set
xa9 is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( xa9 <= IR . b1 & not b1 <= CP9 . f ) } is set
union { H4(b1) where b1 is Element of rng IR : b1 in f9 } is set
yb is set
xa9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . xa9 is Element of the carrier of R
ya9 is Element of the carrier of R
f1 is Element of the carrier of R
g1 is set
Rn is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . Rn is Element of the carrier of R
g1 is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( g1 <= IR . b1 & not b1 <= CP9 . f ) } is set
xb is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( xb <= IR . b1 & not b1 <= CP9 . f ) } is set
xb is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( xb <= IR . b1 & not b1 <= CP9 . f ) } is set
ya is Element of f9
yb is Element of rng IR
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : ( yb <= IR . b1 & not b1 <= CP9 . f ) } is set
ya is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
IR . ya is Element of the carrier of R
[((IR * n) . f),((IR * n) . (f + 1))] is V13() non empty Element of the carrier of [:R,R:]
[:R,R:] is non empty strict RelStr
the carrier of [:R,R:] is non empty set
R is RelStr
the carrier of R is set
bool the carrier of R is non empty set
IR is Element of bool the carrier of R
{} the carrier of R is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() strongly_connected ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() Element of bool the carrier of R
CR is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
R is RelStr
IR is RelStr
[:R,IR:] is strict RelStr
CR is V81() reflexive transitive RelStr
f is V81() reflexive transitive RelStr
[:CR,f:] is strict V81() reflexive transitive RelStr
QOE is non empty RelStr
S is non empty RelStr
[:QOE,S:] is non empty strict RelStr
the carrier of [:QOE,S:] is non empty set
[:NAT, the carrier of [:QOE,S:]:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of [:QOE,S:]:] is non empty non trivial non finite set
n is Relation-like NAT -defined the carrier of [:QOE,S:] -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of [:QOE,S:]) Element of bool [:NAT, the carrier of [:QOE,S:]:]
the carrier of QOE is non empty set
[:NAT, the carrier of QOE:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of QOE:] is non empty non trivial non finite set
n1 is Relation-like NAT -defined the carrier of QOE -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of QOE) Element of bool [:NAT, the carrier of QOE:]
l is Relation-like NAT -defined the carrier of QOE -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of QOE) Element of bool [:NAT, the carrier of QOE:]
k is Relation-like NAT -defined the carrier of QOE -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of QOE) Element of bool [:NAT, the carrier of QOE:]
a is Relation-like NAT -defined NAT -valued Function-like non empty V19( NAT ) V20( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]
l * a is Relation-like NAT -defined the carrier of QOE -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of QOE) subsequence of l
the carrier of S is non empty set
[:NAT, the carrier of S:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of S:] is non empty non trivial non finite set
b is Relation-like NAT -defined the carrier of S -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of S) Element of bool [:NAT, the carrier of S:]
S is Relation-like NAT -defined the carrier of S -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of S) Element of bool [:NAT, the carrier of S:]
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
CP9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
S . CP9 is Element of the carrier of S
S . f is Element of the carrier of S
a . CP9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n . (a . CP9) is Element of the carrier of [:QOE,S:]
a . f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n . (a . f) is Element of the carrier of [:QOE,S:]
dom a is non empty countable V267() V268() V269() V270() V271() V272() V281() V283() Element of bool NAT
dom k is non empty countable V267() V268() V269() V270() V271() V272() V281() V283() Element of bool NAT
k . CP9 is Element of the carrier of QOE
l . (a . CP9) is Element of the carrier of QOE
(n . (a . CP9)) `1 is Element of the carrier of QOE
k . f is Element of the carrier of QOE
l . (a . f) is Element of the carrier of QOE
(n . (a . f)) `1 is Element of the carrier of QOE
f is Element of the carrier of [:QOE,S:]
f `1 is Element of the carrier of QOE
f9 is Element of the carrier of [:QOE,S:]
f9 `1 is Element of the carrier of QOE
f `2 is Element of the carrier of S
f9 `2 is Element of the carrier of S
bool the carrier of [:QOE,S:] is non empty set
n is non empty Element of bool the carrier of [:QOE,S:]
([:QOE,S:],n) is Element of bool (bool the carrier of [:QOE,S:])
bool (bool the carrier of [:QOE,S:]) is non empty set
n1 is non empty Element of bool the carrier of [:QOE,S:]
([:QOE,S:],n1) is Element of bool (bool the carrier of [:QOE,S:])
the carrier of R is set
QOE is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
the carrier of IR is set
[:QOE, the carrier of IR:] is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
[: the carrier of R, the carrier of IR:] is Relation-like set
the carrier of IR is set
the carrier of R is set
QOE is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
[: the carrier of R,QOE:] is Relation-like non-empty empty-yielding RAT -valued INT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
[: the carrier of R, the carrier of IR:] is Relation-like set
the carrier of R is set
the carrier of IR is set
[: the carrier of R, the carrier of IR:] is Relation-like set
the carrier of R is set
the carrier of IR is set
[: the carrier of R, the carrier of IR:] is Relation-like set
R is RelStr
IR is RelStr
the carrier of IR is set
the InternalRel of IR is Relation-like the carrier of IR -defined the carrier of IR -valued Element of bool [: the carrier of IR, the carrier of IR:]
[: the carrier of IR, the carrier of IR:] is Relation-like set
bool [: the carrier of IR, the carrier of IR:] is non empty set
QOE is non empty RelStr
the carrier of QOE is non empty set
S is non empty RelStr
the carrier of S is non empty set
[: the carrier of QOE, the carrier of S:] is Relation-like non empty set
bool [: the carrier of QOE, the carrier of S:] is non empty set
f9 is Relation-like the carrier of QOE -defined the carrier of S -valued Function-like non empty V19( the carrier of QOE) V20( the carrier of QOE, the carrier of S) Element of bool [: the carrier of QOE, the carrier of S:]
rng f9 is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
[:NAT, the carrier of S:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of S:] is non empty non trivial non finite set
[: the carrier of S, the carrier of QOE:] is Relation-like non empty set
bool [: the carrier of S, the carrier of QOE:] is non empty set
f9 " is Relation-like Function-like set
n1 is Relation-like the carrier of S -defined the carrier of QOE -valued Function-like non empty V19( the carrier of S) V20( the carrier of S, the carrier of QOE) Element of bool [: the carrier of S, the carrier of QOE:]
n is Relation-like NAT -defined the carrier of S -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of S) Element of bool [:NAT, the carrier of S:]
[:NAT, the carrier of QOE:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of QOE:] is non empty non trivial non finite set
l is Relation-like NAT -defined the carrier of QOE -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of QOE) Element of bool [:NAT, the carrier of QOE:]
k is Relation-like NAT -defined the carrier of QOE -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of QOE) Element of bool [:NAT, the carrier of QOE:]
b is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
a is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
k . a is Element of the carrier of QOE
k . b is Element of the carrier of QOE
CP9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
S is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
k . S is Element of the carrier of QOE
f9 . (k . S) is Element of the carrier of S
n . S is Element of the carrier of S
(f9 ") . (n . S) is set
f9 . ((f9 ") . (n . S)) is set
k . CP9 is Element of the carrier of QOE
f9 . (k . CP9) is Element of the carrier of S
n . CP9 is Element of the carrier of S
(f9 ") . (n . CP9) is set
f9 . ((f9 ") . (n . CP9)) is set
n is non empty Element of bool the carrier of S
(S,n) is Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
n1 is non empty Element of bool the carrier of S
(S,n1) is Element of bool (bool the carrier of S)
the carrier of R is set
[: the carrier of R, the carrier of IR:] is Relation-like set
bool [: the carrier of R, the carrier of IR:] is non empty set
QOE is Relation-like the carrier of R -defined the carrier of IR -valued Function-like V20( the carrier of R, the carrier of IR) Element of bool [: the carrier of R, the carrier of IR:]
QOE is set
[QOE,QOE] is V13() non empty set
{QOE,QOE} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,QOE},{QOE}} is non empty finite V34() countable set
QOE is set
S is set
f9 is set
[QOE,S] is V13() non empty set
{QOE,S} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,S},{QOE}} is non empty finite V34() countable set
[S,f9] is V13() non empty set
{S,f9} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,f9},{S}} is non empty finite V34() countable set
[QOE,f9] is V13() non empty set
{QOE,f9} is non empty finite countable set
{{QOE,f9},{QOE}} is non empty finite V34() countable set
R is Relation-like 1 -defined Function-like V19(1) V74() RelStr-yielding set
product R is strict RelStr
IR is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() Element of 1
R . IR is RelStr
{0} is functional non empty trivial finite V34() 1 -element with_common_domain countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
the carrier of (R . IR) is set
CR is Relation-like Function-like set
dom CR is set
f is set
CR . f is set
0 .--> f is Relation-like NAT -defined {0} -defined Function-like one-to-one finite countable set
{0} --> f is Relation-like {0} -defined {f} -valued Function-like constant non empty V19({0}) V20({0},{f}) finite countable Element of bool [:{0},{f}:]
{f} is non empty trivial finite 1 -element countable set
[:{0},{f}:] is Relation-like non empty finite countable set
bool [:{0},{f}:] is non empty finite V34() countable set
dom (0 .--> f) is functional trivial finite V34() with_common_domain countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool {0}
bool {0} is non empty finite V34() countable set
{0} is functional non empty trivial finite V34() 1 -element with_common_domain countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of bool NAT
Carrier R is Relation-like 1 -defined Function-like V19(1) set
dom (Carrier R) is finite countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool 1
bool 1 is non empty finite V34() countable set
S is set
R . S is set
(Carrier R) . S is set
(0 .--> f) . S is set
f9 is 1-sorted
the carrier of f9 is set
product (Carrier R) is functional with_common_domain product-like set
the carrier of (product R) is set
[: the carrier of (R . IR), the carrier of (product R):] is Relation-like set
bool [: the carrier of (R . IR), the carrier of (product R):] is non empty set
the Relation-like Function-like Element of product (Carrier R) is Relation-like Function-like Element of product (Carrier R)
R . 0 is set
(Carrier R) . 0 is set
S is 1-sorted
the carrier of S is set
f9 is Relation-like Function-like set
dom f9 is set
f is Relation-like the carrier of (R . IR) -defined the carrier of (product R) -valued Function-like V20( the carrier of (R . IR), the carrier of (product R)) Element of bool [: the carrier of (R . IR), the carrier of (product R):]
S is set
rng R is set
dom R is finite countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool 1
f9 is set
R . f9 is set
R . 0 is set
S is Relation-like 1 -defined Function-like V19(1) V74() RelStr-yielding non-Empty set
product S is non empty strict RelStr
n is set
f is Relation-like the carrier of (R . IR) -defined the carrier of (product R) -valued Function-like V20( the carrier of (R . IR), the carrier of (product R)) Element of bool [: the carrier of (R . IR), the carrier of (product R):]
dom f is Element of bool the carrier of (R . IR)
bool the carrier of (R . IR) is non empty set
n1 is set
f . n is set
f . n1 is set
0 .--> n is Relation-like NAT -defined {0} -defined Function-like one-to-one finite countable set
{0} --> n is Relation-like {0} -defined {n} -valued Function-like constant non empty V19({0}) V20({0},{n}) finite countable Element of bool [:{0},{n}:]
{n} is non empty trivial finite 1 -element countable set
[:{0},{n}:] is Relation-like non empty finite countable set
bool [:{0},{n}:] is non empty finite V34() countable set
[:{0},{n}:] is Relation-like non empty finite countable set
0 .--> n1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite countable set
{0} --> n1 is Relation-like {0} -defined {n1} -valued Function-like constant non empty V19({0}) V20({0},{n1}) finite countable Element of bool [:{0},{n1}:]
{n1} is non empty trivial finite 1 -element countable set
[:{0},{n1}:] is Relation-like non empty finite countable set
bool [:{0},{n1}:] is non empty finite V34() countable set
[:{0},{n1}:] is Relation-like non empty finite countable set
[0,n] is V13() non empty set
{0,n} is non empty finite countable set
{{0,n},{0}} is non empty finite V34() countable set
l is set
k is set
[l,k] is V13() non empty set
{l,k} is non empty finite countable set
{l} is non empty trivial finite 1 -element countable set
{{l,k},{l}} is non empty finite V34() countable set
n is set
rng f is Element of bool the carrier of (product R)
bool the carrier of (product R) is non empty set
n1 is Relation-like Function-like set
dom n1 is set
(Carrier R) . 0 is set
n1 . 0 is set
0 .--> (n1 . 0) is Relation-like NAT -defined {0} -defined Function-like one-to-one finite countable set
{0} --> (n1 . 0) is Relation-like {0} -defined {(n1 . 0)} -valued Function-like constant non empty V19({0}) V20({0},{(n1 . 0)}) finite countable Element of bool [:{0},{(n1 . 0)}:]
{(n1 . 0)} is non empty trivial finite 1 -element countable set
[:{0},{(n1 . 0)}:] is Relation-like non empty finite countable set
bool [:{0},{(n1 . 0)}:] is non empty finite V34() countable set
f . (n1 . 0) is set
l is 1-sorted
the carrier of l is set
l is 1-sorted
the carrier of l is set
QOE is non empty RelStr
the carrier of QOE is non empty set
f9 is non empty RelStr
the carrier of f9 is non empty set
[: the carrier of QOE, the carrier of f9:] is Relation-like non empty set
bool [: the carrier of QOE, the carrier of f9:] is non empty set
n is Relation-like the carrier of QOE -defined the carrier of f9 -valued Function-like non empty V19( the carrier of QOE) V20( the carrier of QOE, the carrier of f9) Element of bool [: the carrier of QOE, the carrier of f9:]
n1 is Element of the carrier of QOE
n . n1 is Element of the carrier of f9
l is Element of the carrier of QOE
n . l is Element of the carrier of f9
0 .--> n1 is Relation-like NAT -defined {0} -defined the carrier of QOE -valued Function-like one-to-one finite countable set
{0} --> n1 is Relation-like {0} -defined the carrier of QOE -valued {n1} -valued Function-like constant non empty V19({0}) V20({0},{n1}) finite countable Element of bool [:{0},{n1}:]
{n1} is non empty trivial finite 1 -element countable set
[:{0},{n1}:] is Relation-like non empty finite countable set
bool [:{0},{n1}:] is non empty finite V34() countable set
0 .--> l is Relation-like NAT -defined {0} -defined the carrier of QOE -valued Function-like one-to-one finite countable set
{0} --> l is Relation-like {0} -defined the carrier of QOE -valued {l} -valued Function-like constant non empty V19({0}) V20({0},{l}) finite countable Element of bool [:{0},{l}:]
{l} is non empty trivial finite 1 -element countable set
[:{0},{l}:] is Relation-like non empty finite countable set
bool [:{0},{l}:] is non empty finite V34() countable set
b is Relation-like Function-like set
S is Relation-like Function-like set
CP9 is set
R . CP9 is set
b . CP9 is set
S . CP9 is set
f is RelStr
the carrier of f is set
f9 is Element of the carrier of f
f is Element of the carrier of f
k is Relation-like Function-like set
a is Relation-like Function-like set
k is Relation-like Function-like set
a is Relation-like Function-like set
k . 0 is set
a . 0 is set
b is RelStr
the carrier of b is set
S is Element of the carrier of b
CP9 is Element of the carrier of b
0 .--> n1 is Relation-like NAT -defined {0} -defined the carrier of QOE -valued Function-like one-to-one finite countable set
{0} --> n1 is Relation-like {0} -defined the carrier of QOE -valued {n1} -valued Function-like constant non empty V19({0}) V20({0},{n1}) finite countable Element of bool [:{0},{n1}:]
{n1} is non empty trivial finite 1 -element countable set
[:{0},{n1}:] is Relation-like non empty finite countable set
bool [:{0},{n1}:] is non empty finite V34() countable set
0 .--> l is Relation-like NAT -defined {0} -defined the carrier of QOE -valued Function-like one-to-one finite countable set
{0} --> l is Relation-like {0} -defined the carrier of QOE -valued {l} -valued Function-like constant non empty V19({0}) V20({0},{l}) finite countable Element of bool [:{0},{l}:]
{l} is non empty trivial finite 1 -element countable set
[:{0},{l}:] is Relation-like non empty finite countable set
bool [:{0},{l}:] is non empty finite V34() countable set
f is Relation-like the carrier of (R . IR) -defined the carrier of (product R) -valued Function-like V20( the carrier of (R . IR), the carrier of (product R)) Element of bool [: the carrier of (R . IR), the carrier of (product R):]
f is Relation-like the carrier of (R . IR) -defined the carrier of (product R) -valued Function-like V20( the carrier of (R . IR), the carrier of (product R)) Element of bool [: the carrier of (R . IR), the carrier of (product R):]
R is set
bool R is non empty set
IR is Relation-like R -defined Function-like V19(R) V74() RelStr-yielding set
CR is Element of bool R
IR | CR is Relation-like R -defined CR -defined R -defined Function-like V19(CR) set
f is set
rng (IR | CR) is set
dom (IR | CR) is Element of bool CR
bool CR is non empty set
QOE is set
(IR | CR) . QOE is set
IR . QOE is set
dom IR is Element of bool R
rng IR is set
R is non empty V25() V29() finite cardinal countable ext-real positive non negative set
IR is Relation-like R -defined Function-like V19(R) V74() RelStr-yielding set
product IR is strict RelStr
Carrier IR is Relation-like R -defined Function-like V19(R) set
product (Carrier IR) is functional with_common_domain product-like set
CR is set
dom (Carrier IR) is finite countable Element of bool R
bool R is non empty finite V34() countable set
f is 1-sorted
rng IR is set
dom IR is finite countable Element of bool R
QOE is set
IR . QOE is set
(Carrier IR) . QOE is set
S is 1-sorted
the carrier of S is set
f9 is Relation-like Function-like set
dom f9 is set
CR is Relation-like Function-like set
dom CR is set
QOE is Relation-like Function-like set
dom QOE is set
S is set
QOE . S is set
(Carrier IR) . S is set
IR . S is set
f9 is RelStr
the carrier of f9 is set
choose ((Carrier IR) . S) is Element of (Carrier IR) . S
n is 1-sorted
the carrier of n is set
QOE is Relation-like Function-like set
dom QOE is set
R is non empty V25() V29() finite cardinal countable ext-real positive non negative set
R + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
bool (R + 1) is non empty finite V34() countable set
IR is Relation-like R + 1 -defined Function-like V19(R + 1) V74() RelStr-yielding set
product IR is strict RelStr
CR is finite countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool (R + 1)
IR | CR is Relation-like R + 1 -defined CR -defined R + 1 -defined Function-like V19(CR) finite countable V74() RelStr-yielding set
product (IR | CR) is strict RelStr
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() Element of R + 1
IR . f is RelStr
[:(product (IR | CR)),(IR . f):] is strict RelStr
the carrier of (product (IR | CR)) is set
the carrier of (IR . f) is set
[: the carrier of (product (IR | CR)), the carrier of (IR . f):] is Relation-like set
the carrier of (product IR) is set
Carrier (IR | CR) is Relation-like CR -defined Function-like V19(CR) set
dom (Carrier (IR | CR)) is finite countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool CR
bool CR is non empty finite V34() countable set
rng IR is set
n1 is 1-sorted
dom IR is finite countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool (R + 1)
l is set
IR . l is set
{R} is non empty trivial finite V34() 1 -element countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
R \/ {R} is non empty finite countable set
(IR | CR) . l is set
dom (IR | CR) is finite countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool CR
rng (IR | CR) is finite countable set
k is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
[:k, the carrier of (IR . f):] is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
a is set
k is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
[:a,k:] is Relation-like non-empty empty-yielding RAT -valued INT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
dom {} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
the carrier of [:(product (IR | CR)),(IR . f):] is set
k is set
{} . k is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() V250() V251() ext-real non positive non negative V256() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
[: the carrier of [:(product (IR | CR)),(IR . f):], the carrier of (product IR):] is Relation-like set
bool [: the carrier of [:(product (IR | CR)),(IR . f):], the carrier of (product IR):] is non empty set
k is Relation-like the carrier of [:(product (IR | CR)),(IR . f):] -defined the carrier of (product IR) -valued Function-like V20( the carrier of [:(product (IR | CR)),(IR . f):], the carrier of (product IR)) Element of bool [: the carrier of [:(product (IR | CR)),(IR . f):], the carrier of (product IR):]
k is Relation-like R + 1 -defined Function-like V19(R + 1) V74() RelStr-yielding non-Empty set
k . f is non empty RelStr
b is 1-sorted
rng (IR | CR) is finite countable set
dom (IR | CR) is finite countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool CR
S is set
(IR | CR) . S is set
dom IR is finite countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool (R + 1)
IR . S is set
rng IR is set
b is non empty set
a is non empty set
[:b,a:] is Relation-like non empty set
S is non empty RelStr
the carrier of S is non empty set
CP9 is non empty set
n1 is non empty set
f is Element of CP9
f is Element of [:b,a:]
f `1 is set
f `2 is set
product (Carrier (IR | CR)) is functional with_common_domain product-like set
x is Element of b
xa is Relation-like Function-like set
y is Element of a
R .--> y is Relation-like {R} -defined a -valued Function-like one-to-one finite countable set
{R} is non empty trivial finite V34() 1 -element countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{R} --> y is Relation-like {R} -defined a -valued {y} -valued Function-like constant non empty V19({R}) V20({R},{y}) finite countable Element of bool [:{R},{y}:]
{y} is non empty trivial finite 1 -element countable set
[:{R},{y}:] is Relation-like non empty finite countable set
bool [:{R},{y}:] is non empty finite V34() countable set
xa +* (R .--> y) is Relation-like Function-like set
yb is Relation-like Function-like set
xa9 is Relation-like Function-like set
dom xa is set
ya9 is Relation-like Function-like set
dom ya9 is set
dom xa9 is set
dom (R .--> y) is trivial finite V34() countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool {R}
bool {R} is non empty finite V34() countable set
(dom xa) \/ (dom (R .--> y)) is set
R \/ {R} is non empty finite countable set
Carrier IR is Relation-like R + 1 -defined Function-like V19(R + 1) set
dom (Carrier IR) is finite countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool (R + 1)
ya9 is set
xa9 . ya9 is set
xa . ya9 is set
(IR | CR) . ya9 is set
(Carrier (IR | CR)) . ya9 is set
IR . ya9 is set
(Carrier IR) . ya9 is set
f1 is 1-sorted
the carrier of f1 is set
g1 is 1-sorted
the carrier of g1 is set
f1 is Relation-like Function-like set
dom f1 is set
xa9 . ya9 is set
(R .--> y) . R is set
(Carrier IR) . f is set
(Carrier IR) . ya9 is set
f1 is 1-sorted
the carrier of f1 is set
product (Carrier IR) is functional with_common_domain product-like set
ya is Relation-like Function-like set
dom ya is set
ya is Element of n1
[xa,y] is V13() non empty set
{xa,y} is non empty finite countable set
{xa} is functional non empty trivial finite 1 -element with_common_domain countable set
{{xa,y},{xa}} is non empty finite V34() countable set
[:CP9,n1:] is Relation-like non empty set
bool [:CP9,n1:] is non empty set
f is Relation-like CP9 -defined n1 -valued Function-like non empty V19(CP9) V20(CP9,n1) Element of bool [:CP9,n1:]
the carrier of [:(product (IR | CR)),(IR . f):] is set
[: the carrier of [:(product (IR | CR)),(IR . f):], the carrier of (product IR):] is Relation-like set
bool [: the carrier of [:(product (IR | CR)),(IR . f):], the carrier of (product IR):] is non empty set
l is non empty RelStr
the carrier of l is non empty set
[: the carrier of S, the carrier of l:] is Relation-like non empty set
bool [: the carrier of S, the carrier of l:] is non empty set
f is Relation-like the carrier of [:(product (IR | CR)),(IR . f):] -defined the carrier of (product IR) -valued Function-like V20( the carrier of [:(product (IR | CR)),(IR . f):], the carrier of (product IR)) Element of bool [: the carrier of [:(product (IR | CR)),(IR . f):], the carrier of (product IR):]
x is set
f is Relation-like the carrier of [:(product (IR | CR)),(IR . f):] -defined the carrier of (product IR) -valued Function-like V20( the carrier of [:(product (IR | CR)),(IR . f):], the carrier of (product IR)) Element of bool [: the carrier of [:(product (IR | CR)),(IR . f):], the carrier of (product IR):]
dom f is Element of bool the carrier of [:(product (IR | CR)),(IR . f):]
bool the carrier of [:(product (IR | CR)),(IR . f):] is non empty set
y is set
f . x is set
f . y is set
xa is Relation-like Function-like set
xb is Element of a
[xa,xb] is V13() non empty set
{xa,xb} is non empty finite countable set
{xa} is functional non empty trivial finite 1 -element with_common_domain countable set
{{xa,xb},{xa}} is non empty finite V34() countable set
R .--> xb is Relation-like {R} -defined a -valued Function-like one-to-one finite countable set
{R} is non empty trivial finite V34() 1 -element countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{R} --> xb is Relation-like {R} -defined a -valued {xb} -valued Function-like constant non empty V19({R}) V20({R},{xb}) finite countable Element of bool [:{R},{xb}:]
{xb} is non empty trivial finite 1 -element countable set
[:{R},{xb}:] is Relation-like non empty finite countable set
bool [:{R},{xb}:] is non empty finite V34() countable set
xa +* (R .--> xb) is Relation-like Function-like set
ya is Relation-like Function-like set
yb is Element of a
[ya,yb] is V13() non empty set
{ya,yb} is non empty finite countable set
{ya} is functional non empty trivial finite 1 -element with_common_domain countable set
{{ya,yb},{ya}} is non empty finite V34() countable set
R .--> yb is Relation-like {R} -defined a -valued Function-like one-to-one finite countable set
{R} --> yb is Relation-like {R} -defined a -valued {yb} -valued Function-like constant non empty V19({R}) V20({R},{yb}) finite countable Element of bool [:{R},{yb}:]
{yb} is non empty trivial finite 1 -element countable set
[:{R},{yb}:] is Relation-like non empty finite countable set
bool [:{R},{yb}:] is non empty finite V34() countable set
ya +* (R .--> yb) is Relation-like Function-like set
product (Carrier (IR | CR)) is functional with_common_domain product-like set
dom (R .--> xb) is trivial finite V34() countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool {R}
bool {R} is non empty finite V34() countable set
dom (R .--> yb) is trivial finite V34() countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool {R}
dom xa is set
xa9 is Relation-like Function-like set
dom xa9 is set
R /\ {R} is finite countable V267() V268() V269() V270() V271() V272() V283() V284() V285() set
xa9 is set
dom ya is set
xa9 is Relation-like Function-like set
dom xa9 is set
ya9 is Relation-like Function-like set
dom ya9 is set
xa9 is set
ya9 is set
[xa9,ya9] is V13() non empty set
{xa9,ya9} is non empty finite countable set
{xa9} is non empty trivial finite 1 -element countable set
{{xa9,ya9},{xa9}} is non empty finite V34() countable set
xa . xa9 is set
(dom xa) \/ (dom (R .--> xb)) is set
(ya +* (R .--> yb)) . xa9 is set
(dom ya) \/ (dom (R .--> yb)) is set
f1 is Relation-like Function-like set
dom f1 is set
g1 is Relation-like Function-like set
dom g1 is set
f1 is Relation-like Function-like set
dom f1 is set
g1 is Relation-like Function-like set
dom g1 is set
ya . xa9 is set
(xa +* (R .--> xb)) . xa9 is set
f1 is Relation-like Function-like set
dom f1 is set
g1 is Relation-like Function-like set
dom g1 is set
f1 is Relation-like Function-like set
dom f1 is set
g1 is Relation-like Function-like set
dom g1 is set
(xa +* (R .--> xb)) . R is set
(R .--> yb) . R is set
(R .--> xb) . R is set
x is set
rng f is Element of bool the carrier of (product IR)
bool the carrier of (product IR) is non empty set
Carrier IR is Relation-like R + 1 -defined Function-like V19(R + 1) set
product (Carrier IR) is functional with_common_domain product-like set
dom (Carrier IR) is finite countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool (R + 1)
y is Relation-like Function-like set
dom y is set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : not R + 1 <= b1 } is set
y | R is Relation-like Function-like finite countable set
y . R is set
[(y | R),(y . R)] is V13() non empty set
{(y | R),(y . R)} is non empty finite countable set
{(y | R)} is functional non empty trivial finite V34() 1 -element with_common_domain countable set
{{(y | R),(y . R)},{(y | R)}} is non empty finite V34() countable set
dom (y | R) is finite countable set
(dom y) /\ R is finite countable set
(R + 1) /\ R is finite countable V267() V268() V269() V270() V271() V272() V283() V284() V285() set
yb is set
(y | R) . yb is set
y . yb is set
(Carrier IR) . yb is set
IR . yb is set
(IR | CR) . yb is set
(Carrier (IR | CR)) . yb is set
xa9 is 1-sorted
the carrier of xa9 is set
ya9 is 1-sorted
the carrier of ya9 is set
IR . R is set
(Carrier IR) . R is set
yb is 1-sorted
the carrier of yb is set
f . [(y | R),(y . R)] is set
yb is Relation-like Function-like set
xa9 is Element of a
[yb,xa9] is V13() non empty set
{yb,xa9} is non empty finite countable set
{yb} is functional non empty trivial finite 1 -element with_common_domain countable set
{{yb,xa9},{yb}} is non empty finite V34() countable set
R .--> xa9 is Relation-like {R} -defined a -valued Function-like one-to-one finite countable set
{R} --> xa9 is Relation-like {R} -defined a -valued {xa9} -valued Function-like constant non empty V19({R}) V20({R},{xa9}) finite countable Element of bool [:{R},{xa9}:]
{xa9} is non empty trivial finite 1 -element countable set
[:{R},{xa9}:] is Relation-like non empty finite countable set
bool [:{R},{xa9}:] is non empty finite V34() countable set
yb +* (R .--> xa9) is Relation-like Function-like set
ya9 is set
f1 is set
[ya9,f1] is V13() non empty set
{ya9,f1} is non empty finite countable set
{ya9} is non empty trivial finite 1 -element countable set
{{ya9,f1},{ya9}} is non empty finite V34() countable set
R .--> (y . R) is Relation-like {R} -defined Function-like one-to-one finite countable set
{R} --> (y . R) is Relation-like {R} -defined {(y . R)} -valued Function-like constant non empty V19({R}) V20({R},{(y . R)}) finite countable Element of bool [:{R},{(y . R)}:]
{(y . R)} is non empty trivial finite 1 -element countable set
[:{R},{(y . R)}:] is Relation-like non empty finite countable set
bool [:{R},{(y . R)}:] is non empty finite V34() countable set
(y | R) +* (R .--> (y . R)) is Relation-like Function-like finite countable set
dom ((y | R) +* (R .--> (y . R))) is finite countable set
dom (R .--> (y . R)) is trivial finite V34() countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool {R}
(dom (y | R)) \/ (dom (R .--> (y . R))) is finite countable set
R \/ {R} is non empty finite countable set
((y | R) +* (R .--> (y . R))) . ya9 is set
(R .--> (y . R)) . ya9 is set
y . ya9 is set
(y | R) . ya9 is set
y . ya9 is set
(R .--> (y . R)) . ya9 is set
(y | R) . ya9 is set
y . ya9 is set
x is Element of the carrier of S
f . x is set
xa is Relation-like Function-like set
xb is Element of a
[xa,xb] is V13() non empty set
{xa,xb} is non empty finite countable set
{xa} is functional non empty trivial finite 1 -element with_common_domain countable set
{{xa,xb},{xa}} is non empty finite V34() countable set
R .--> xb is Relation-like {R} -defined a -valued Function-like one-to-one finite countable set
{R} --> xb is Relation-like {R} -defined a -valued {xb} -valued Function-like constant non empty V19({R}) V20({R},{xb}) finite countable Element of bool [:{R},{xb}:]
{xb} is non empty trivial finite 1 -element countable set
[:{R},{xb}:] is Relation-like non empty finite countable set
bool [:{R},{xb}:] is non empty finite V34() countable set
xa +* (R .--> xb) is Relation-like Function-like set
f9 is Relation-like the carrier of S -defined the carrier of l -valued Function-like non empty V19( the carrier of S) V20( the carrier of S, the carrier of l) Element of bool [: the carrier of S, the carrier of l:]
f9 . x is Element of the carrier of l
y is Element of the carrier of S
f . y is set
ya is Relation-like Function-like set
yb is Element of a
[ya,yb] is V13() non empty set
{ya,yb} is non empty finite countable set
{ya} is functional non empty trivial finite 1 -element with_common_domain countable set
{{ya,yb},{ya}} is non empty finite V34() countable set
R .--> yb is Relation-like {R} -defined a -valued Function-like one-to-one finite countable set
{R} --> yb is Relation-like {R} -defined a -valued {yb} -valued Function-like constant non empty V19({R}) V20({R},{yb}) finite countable Element of bool [:{R},{yb}:]
{yb} is non empty trivial finite 1 -element countable set
[:{R},{yb}:] is Relation-like non empty finite countable set
bool [:{R},{yb}:] is non empty finite V34() countable set
ya +* (R .--> yb) is Relation-like Function-like set
[xa,xb] `1 is set
[xa,xb] `2 is set
dom xa is set
xa9 is Relation-like Function-like set
dom xa9 is set
dom (R .--> xb) is trivial finite V34() countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool {R}
(dom xa) \/ (dom (R .--> xb)) is set
dom ya is set
xa9 is Relation-like Function-like set
dom xa9 is set
dom (R .--> yb) is trivial finite V34() countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool {R}
(dom ya) \/ (dom (R .--> yb)) is set
[x,y] is V13() non empty Element of the carrier of [:S,S:]
[:S,S:] is non empty strict RelStr
the carrier of [:S,S:] is non empty set
{x,y} is non empty finite countable set
{x} is non empty trivial finite 1 -element countable set
{{x,y},{x}} is non empty finite V34() countable set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like non empty set
bool [: the carrier of S, the carrier of S:] is non empty set
the InternalRel of (product (IR | CR)) is Relation-like the carrier of (product (IR | CR)) -defined the carrier of (product (IR | CR)) -valued Element of bool [: the carrier of (product (IR | CR)), the carrier of (product (IR | CR)):]
[: the carrier of (product (IR | CR)), the carrier of (product (IR | CR)):] is Relation-like set
bool [: the carrier of (product (IR | CR)), the carrier of (product (IR | CR)):] is non empty set
the InternalRel of (IR . f) is Relation-like the carrier of (IR . f) -defined the carrier of (IR . f) -valued Element of bool [: the carrier of (IR . f), the carrier of (IR . f):]
[: the carrier of (IR . f), the carrier of (IR . f):] is Relation-like set
bool [: the carrier of (IR . f), the carrier of (IR . f):] is non empty set
[" the InternalRel of (product (IR | CR)), the InternalRel of (IR . f)"] is Relation-like [: the carrier of (product (IR | CR)), the carrier of (IR . f):] -defined [: the carrier of (product (IR | CR)), the carrier of (IR . f):] -valued Element of bool [:[: the carrier of (product (IR | CR)), the carrier of (IR . f):],[: the carrier of (product (IR | CR)), the carrier of (IR . f):]:]
[:[: the carrier of (product (IR | CR)), the carrier of (IR . f):],[: the carrier of (product (IR | CR)), the carrier of (IR . f):]:] is Relation-like set
bool [:[: the carrier of (product (IR | CR)), the carrier of (IR . f):],[: the carrier of (product (IR | CR)), the carrier of (IR . f):]:] is non empty set
[x,y] `1 is Element of the carrier of S
([x,y] `1) `1 is set
[x,y] `2 is Element of the carrier of S
([x,y] `2) `1 is set
[(([x,y] `1) `1),(([x,y] `2) `1)] is V13() non empty set
{(([x,y] `1) `1),(([x,y] `2) `1)} is non empty finite countable set
{(([x,y] `1) `1)} is non empty trivial finite 1 -element countable set
{{(([x,y] `1) `1),(([x,y] `2) `1)},{(([x,y] `1) `1)}} is non empty finite V34() countable set
([x,y] `1) `2 is set
([x,y] `2) `2 is set
[(([x,y] `1) `2),(([x,y] `2) `2)] is V13() non empty set
{(([x,y] `1) `2),(([x,y] `2) `2)} is non empty finite countable set
{(([x,y] `1) `2)} is non empty trivial finite 1 -element countable set
{{(([x,y] `1) `2),(([x,y] `2) `2)},{(([x,y] `1) `2)}} is non empty finite V34() countable set
[ya,yb] `1 is set
[xa,ya] is V13() non empty set
{xa,ya} is functional non empty finite countable set
{{xa,ya},{xa}} is non empty finite V34() countable set
xa9 is Element of the carrier of (product (IR | CR))
ya9 is Element of the carrier of (product (IR | CR))
f1 is Relation-like Function-like set
g1 is Relation-like Function-like set
[ya,yb] `2 is set
[xb,yb] is V13() non empty Element of [:a,a:]
[:a,a:] is Relation-like non empty set
{xb,yb} is non empty finite countable set
{{xb,yb},{xb}} is non empty finite V34() countable set
Rn is Element of the carrier of (IR . f)
xni is Element of the carrier of (IR . f)
f2 is set
IR . f2 is set
(xa +* (R .--> xb)) . f2 is set
(ya +* (R .--> yb)) . f2 is set
(R .--> xb) . f2 is set
R is RelStr
the carrier of R is set
xa . f2 is set
(Carrier (IR | CR)) . f2 is set
R is Relation-like Function-like set
dom R is set
(IR | CR) . f2 is set
R is RelStr
the carrier of R is set
R is 1-sorted
the carrier of R is set
R is RelStr
the carrier of R is set
R is RelStr
the carrier of R is set
(R .--> yb) . f2 is set
ya . f2 is set
(Carrier (IR | CR)) . f2 is set
xi is Relation-like Function-like set
dom xi is set
(IR | CR) . f2 is set
xi is 1-sorted
the carrier of xi is set
R is Element of the carrier of R
xi is Element of the carrier of R
ya . f2 is set
(IR | CR) . f2 is set
f1 . f2 is set
g1 . f2 is set
yi is RelStr
the carrier of yi is set
xi is Element of the carrier of yi
yi is Element of the carrier of yi
(R .--> xb) . f2 is set
(R .--> yb) . f2 is set
f9 . y is Element of the carrier of l
yni is Relation-like Function-like set
g2 is Relation-like Function-like set
f1 is Relation-like Function-like set
g1 is Relation-like Function-like set
yni is Relation-like Function-like set
g2 is Relation-like Function-like set
f2 is Relation-like Function-like set
g2 is Relation-like Function-like set
i is set
(IR | CR) . i is set
R is RelStr
xa . i is set
ya . i is set
(Carrier (IR | CR)) . i is set
R is RelStr
the carrier of R is set
yi is 1-sorted
the carrier of yi is set
xi is Relation-like Function-like set
dom xi is set
xi is 1-sorted
the carrier of xi is set
yi is Relation-like Function-like set
dom yi is set
xi is Element of the carrier of R
yi is Element of the carrier of R
xi is Element of the carrier of R
f2 . i is set
yi is Element of the carrier of R
g2 . i is set
IR . i is set
f1 . i is set
g1 . i is set
R2 is RelStr
the carrier of R2 is set
xi2 is Element of the carrier of R2
yi2 is Element of the carrier of R2
(xa +* (R .--> xb)) . i is set
Rn is Relation-like Function-like set
xni is Relation-like Function-like set
f1 . R is set
g1 . R is set
Rn is RelStr
the carrier of Rn is set
xni is Element of the carrier of Rn
yni is Element of the carrier of Rn
[xni,yni] is V13() non empty set
{xni,yni} is non empty finite countable set
{xni} is non empty trivial finite 1 -element countable set
{{xni,yni},{xni}} is non empty finite V34() countable set
(xa +* (R .--> xb)) . R is set
(R .--> xb) . R is set
(ya +* (R .--> yb)) . R is set
(R .--> yb) . R is set
f is Relation-like the carrier of [:(product (IR | CR)),(IR . f):] -defined the carrier of (product IR) -valued Function-like V20( the carrier of [:(product (IR | CR)),(IR . f):], the carrier of (product IR)) Element of bool [: the carrier of [:(product (IR | CR)),(IR . f):], the carrier of (product IR):]
R is Relation-like 1 -defined Function-like V19(1) V74() RelStr-yielding set
product R is strict RelStr
IR is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() Element of 1
R . IR is RelStr
R is non empty V25() V29() finite cardinal countable ext-real positive non negative set
R + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
IR is Relation-like R + 1 -defined Function-like V19(R + 1) V74() RelStr-yielding set
product IR is strict RelStr
bool (R + 1) is non empty finite V34() countable set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : not R + 1 <= b1 } is set
CR is finite countable V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of bool (R + 1)
IR | CR is Relation-like R + 1 -defined CR -defined R + 1 -defined Function-like V19(CR) finite countable V74() RelStr-yielding set
QOE is Relation-like R -defined Function-like V19(R) V74() RelStr-yielding set
S is Element of R
QOE . S is RelStr
IR . S is set
{ b1 where b1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : not R <= b1 } is set
f9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() Element of R + 1
product QOE is strict RelStr
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() Element of R + 1
IR . f is RelStr
product (IR | CR) is strict RelStr
[:(product (IR | CR)),(IR . f):] is strict RelStr
R is Relation-like non-empty empty-yielding {} -defined RAT -valued Function-like one-to-one constant functional empty trivial V19( {} ) V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() V74() RelStr-yielding ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
product R is strict RelStr
the carrier of (product R) is set
the InternalRel of (product R) is Relation-like the carrier of (product R) -defined the carrier of (product R) -valued Element of bool [: the carrier of (product R), the carrier of (product R):]
[: the carrier of (product R), the carrier of (product R):] is Relation-like set
bool [: the carrier of (product R), the carrier of (product R):] is non empty set
QOE is set
S is set
f9 is set
[QOE,S] is V13() non empty set
{QOE,S} is non empty finite countable set
{QOE} is non empty trivial finite 1 -element countable set
{{QOE,S},{QOE}} is non empty finite V34() countable set
[S,f9] is V13() non empty set
{S,f9} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,f9},{S}} is non empty finite V34() countable set
[QOE,f9] is V13() non empty set
{QOE,f9} is non empty finite countable set
{{QOE,f9},{QOE}} is non empty finite V34() countable set
bool the carrier of (product R) is non empty set
QOE is Element of bool the carrier of (product R)
S is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
{} the carrier of (product R) is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() strongly_connected ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() Element of bool the carrier of (product R)
S is functional non empty trivial finite V34() 1 -element with_common_domain countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
f9 is Element of the carrier of (product R)
n is Element of the carrier of (product R)
[n,f9] is V13() non empty set
{n,f9} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,f9},{n}} is non empty finite V34() countable set
R is Relation-like non-empty empty-yielding {} -defined RAT -valued Function-like one-to-one constant functional empty trivial V19( {} ) V25() V29() finite finite-yielding V34() cardinal {} -element Cardinal-yielding countable Function-yielding V44() V74() RelStr-yielding ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V267() V268() V269() V270() V271() V272() V273() V283() V284() V285() V286() set
product R is strict RelStr
{ [b1,b2] where b1, b2 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT : b1 <= b2 } is set
IR is set
[:NAT,NAT:] is Relation-like REAL -defined REAL -valued RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:REAL,REAL:]
[:REAL,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is non empty set
CR is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
[CR,f] is V13() non empty Element of [:NAT,NAT:]
{CR,f} is non empty finite V34() countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{CR} is non empty trivial finite V34() 1 -element countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{{CR,f},{CR}} is non empty finite V34() countable set
() is Relation-like NAT -defined NAT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
R is set
[R,R] is V13() non empty set
{R,R} is non empty finite countable set
{R} is non empty trivial finite 1 -element countable set
{{R,R},{R}} is non empty finite V34() countable set
IR is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
R is set
IR is set
[R,IR] is V13() non empty set
{R,IR} is non empty finite countable set
{R} is non empty trivial finite 1 -element countable set
{{R,IR},{R}} is non empty finite V34() countable set
[IR,R] is V13() non empty set
{IR,R} is non empty finite countable set
{IR} is non empty trivial finite 1 -element countable set
{{IR,R},{IR}} is non empty finite V34() countable set
CR is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
[CR,f] is V13() non empty Element of [:NAT,NAT:]
{CR,f} is non empty finite V34() countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{CR} is non empty trivial finite V34() 1 -element countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{{CR,f},{CR}} is non empty finite V34() countable set
QOE is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
S is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
[QOE,S] is V13() non empty Element of [:NAT,NAT:]
{QOE,S} is non empty finite V34() countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{QOE} is non empty trivial finite V34() 1 -element countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{{QOE,S},{QOE}} is non empty finite V34() countable set
R is set
IR is set
[R,IR] is V13() non empty set
{R,IR} is non empty finite countable set
{R} is non empty trivial finite 1 -element countable set
{{R,IR},{R}} is non empty finite V34() countable set
[IR,R] is V13() non empty set
{IR,R} is non empty finite countable set
{IR} is non empty trivial finite 1 -element countable set
{{IR,R},{IR}} is non empty finite V34() countable set
CR is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
CR is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
CR is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
R is set
IR is set
CR is set
[R,IR] is V13() non empty set
{R,IR} is non empty finite countable set
{R} is non empty trivial finite 1 -element countable set
{{R,IR},{R}} is non empty finite V34() countable set
[IR,CR] is V13() non empty set
{IR,CR} is non empty finite countable set
{IR} is non empty trivial finite 1 -element countable set
{{IR,CR},{IR}} is non empty finite V34() countable set
[R,CR] is V13() non empty set
{R,CR} is non empty finite countable set
{{R,CR},{R}} is non empty finite V34() countable set
f is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
QOE is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
[f,QOE] is V13() non empty Element of [:NAT,NAT:]
{f,QOE} is non empty finite V34() countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{f} is non empty trivial finite V34() 1 -element countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{{f,QOE},{f}} is non empty finite V34() countable set
S is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
[S,f9] is V13() non empty Element of [:NAT,NAT:]
{S,f9} is non empty finite V34() countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{S} is non empty trivial finite V34() 1 -element countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{{S,f9},{S}} is non empty finite V34() countable set
RelStr(# NAT,() #) is non empty strict RelStr
() is non empty RelStr
the carrier of () is non empty set
R is Element of the carrier of ()
IR is Element of the carrier of ()
[R,IR] is V13() non empty Element of the carrier of [:(),():]
[:(),():] is non empty strict RelStr
the carrier of [:(),():] is non empty set
{R,IR} is non empty finite countable set
{R} is non empty trivial finite 1 -element countable set
{{R,IR},{R}} is non empty finite V34() countable set
[IR,R] is V13() non empty Element of the carrier of [:(),():]
{IR,R} is non empty finite countable set
{IR} is non empty trivial finite 1 -element countable set
{{IR,R},{IR}} is non empty finite V34() countable set
(()) is non empty strict antisymmetric RelStr
the InternalRel of () is Relation-like the carrier of () -defined the carrier of () -valued Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
( the carrier of (), the InternalRel of ()) is Relation-like the carrier of () -defined the carrier of () -valued asymmetric Element of bool [: the carrier of (), the carrier of ():]
the InternalRel of () ~ is Relation-like set
the InternalRel of () \ ( the InternalRel of () ~) is Relation-like the carrier of () -defined the carrier of () -valued Element of bool the InternalRel of ()
bool the InternalRel of () is non empty set
RelStr(# the carrier of (),( the carrier of (), the InternalRel of ()) #) is non empty strict RelStr
the InternalRel of (()) is Relation-like the carrier of (()) -defined the carrier of (()) -valued Element of bool [: the carrier of (()), the carrier of (()):]
the carrier of (()) is non empty set
[: the carrier of (()), the carrier of (()):] is Relation-like non empty set
bool [: the carrier of (()), the carrier of (()):] is non empty set
CR is set
f is set
f is V25() V29() finite cardinal countable ext-real non negative set
QOE is Element of the carrier of ()
the InternalRel of (()) -Seg QOE is set
( the InternalRel of (()) -Seg QOE) /\ CR is set
S is set
[S,QOE] is V13() non empty set
{S,QOE} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,QOE},{S}} is non empty finite V34() countable set
f9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
[f9,n] is V13() non empty Element of [:NAT,NAT:]
{f9,n} is non empty finite V34() countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{f9} is non empty trivial finite V34() 1 -element countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{{f9,n},{f9}} is non empty finite V34() countable set
[n,f9] is V13() non empty Element of [:NAT,NAT:]
{n,f9} is non empty finite V34() countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{n} is non empty trivial finite V34() 1 -element countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{{n,f9},{n}} is non empty finite V34() countable set
the InternalRel of () is Relation-like the carrier of () -defined the carrier of () -valued Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
[:NAT, the carrier of ():] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of ():] is non empty non trivial non finite set
IR is Relation-like NAT -defined the carrier of () -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of ()) Element of bool [:NAT, the carrier of ():]
dom IR is non empty countable V267() V268() V269() V270() V271() V272() V281() V283() Element of bool NAT
rng IR is non empty V154(()) V155(()) Element of bool the carrier of ()
bool the carrier of () is non empty set
CR is non empty countable V267() V268() V269() V270() V271() V272() V281() V283() Element of bool NAT
min CR is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
QOE is set
IR . QOE is set
S is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
S + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
IR . (S + 1) is Element of the carrier of ()
IR . S is Element of the carrier of ()
[(IR . (S + 1)),(IR . S)] is V13() non empty Element of the carrier of [:(),():]
{(IR . (S + 1)),(IR . S)} is non empty finite countable set
{(IR . (S + 1))} is non empty trivial finite 1 -element countable set
{{(IR . (S + 1)),(IR . S)},{(IR . (S + 1))}} is non empty finite V34() countable set
f9 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
[f9,n] is V13() non empty Element of [:NAT,NAT:]
{f9,n} is non empty finite V34() countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{f9} is non empty trivial finite V34() 1 -element countable V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() set
{{f9,n},{f9}} is non empty finite V34() countable set
l is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
n1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
R is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
R --> () is Relation-like R -defined {()} -valued Function-like constant V19(R) V20(R,{()}) V27() finite countable V74() RelStr-yielding non-Empty Element of bool [:R,{()}:]
{()} is non empty trivial finite 1 -element countable set
[:R,{()}:] is Relation-like finite countable set
bool [:R,{()}:] is non empty finite V34() countable set
product (R --> ()) is non empty strict RelStr
CR is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
CR --> () is Relation-like CR -defined {()} -valued Function-like constant non empty V19(CR) V20(CR,{()}) V27() finite countable V74() RelStr-yielding non-Empty Element of bool [:CR,{()}:]
[:CR,{()}:] is Relation-like non empty finite countable set
bool [:CR,{()}:] is non empty finite V34() countable set
QOE is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() Element of CR
(CR --> ()) . QOE is non empty RelStr
S is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() Element of CR
(CR --> ()) . S is non empty RelStr
product (CR --> ()) is non empty strict transitive antisymmetric RelStr
R is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
R --> () is Relation-like R -defined {()} -valued Function-like constant V19(R) V20(R,{()}) V27() finite countable V74() RelStr-yielding non-Empty Element of bool [:R,{()}:]
[:R,{()}:] is Relation-like finite countable set
bool [:R,{()}:] is non empty finite V34() countable set
product (R --> ()) is non empty strict RelStr
R is RelStr
[:R,():] is strict RelStr
R is non empty RelStr
IR is non empty RelStr
the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
the InternalRel of IR is Relation-like the carrier of IR -defined the carrier of IR -valued Element of bool [: the carrier of IR, the carrier of IR:]
the carrier of IR is non empty set
[: the carrier of IR, the carrier of IR:] is Relation-like non empty set
bool [: the carrier of IR, the carrier of IR:] is non empty set
(IR) is non empty strict antisymmetric RelStr
( the carrier of IR, the InternalRel of IR) is Relation-like the carrier of IR -defined the carrier of IR -valued asymmetric Element of bool [: the carrier of IR, the carrier of IR:]
the InternalRel of IR ~ is Relation-like set
the InternalRel of IR \ ( the InternalRel of IR ~) is Relation-like the carrier of IR -defined the carrier of IR -valued Element of bool the InternalRel of IR
bool the InternalRel of IR is non empty set
RelStr(# the carrier of IR,( the carrier of IR, the InternalRel of IR) #) is non empty strict RelStr
R is non empty RelStr
the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
f is non empty RelStr
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of bool [: the carrier of f, the carrier of f:]
the carrier of f is non empty set
[: the carrier of f, the carrier of f:] is Relation-like non empty set
bool [: the carrier of f, the carrier of f:] is non empty set
(f) is non empty strict antisymmetric RelStr
( the carrier of f, the InternalRel of f) is Relation-like the carrier of f -defined the carrier of f -valued asymmetric Element of bool [: the carrier of f, the carrier of f:]
the InternalRel of f ~ is Relation-like set
the InternalRel of f \ ( the InternalRel of f ~) is Relation-like the carrier of f -defined the carrier of f -valued Element of bool the InternalRel of f
bool the InternalRel of f is non empty set
RelStr(# the carrier of f,( the carrier of f, the InternalRel of f) #) is non empty strict RelStr
bool the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
f is non empty Element of bool the carrier of R
(R,f) is Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
QOE is non empty Element of bool the carrier of R
(R,QOE) is Element of bool (bool the carrier of R)
f is Relation-like NAT -defined the carrier of R -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
QOE is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
RelStr(# the carrier of R,QOE #) is non empty strict RelStr
f9 is set
n is set
[f9,n] is V13() non empty set
{f9,n} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n},{f9}} is non empty finite V34() countable set
dom the InternalRel of R is Element of bool the carrier of R
rng the InternalRel of R is Element of bool the carrier of R
the InternalRel of RelStr(# the carrier of R,QOE #) is Relation-like the carrier of RelStr(# the carrier of R,QOE #) -defined the carrier of RelStr(# the carrier of R,QOE #) -valued Element of bool [: the carrier of RelStr(# the carrier of R,QOE #), the carrier of RelStr(# the carrier of R,QOE #):]
the carrier of RelStr(# the carrier of R,QOE #) is non empty set
[: the carrier of RelStr(# the carrier of R,QOE #), the carrier of RelStr(# the carrier of R,QOE #):] is Relation-like non empty set
bool [: the carrier of RelStr(# the carrier of R,QOE #), the carrier of RelStr(# the carrier of R,QOE #):] is non empty set
f9 is set
[f9,f9] is V13() non empty set
{f9,f9} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,f9},{f9}} is non empty finite V34() countable set
f9 is set
n is set
n1 is set
[f9,n] is V13() non empty set
{f9,n} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,n},{f9}} is non empty finite V34() countable set
[n,n1] is V13() non empty set
{n,n1} is non empty finite countable set
{n} is non empty trivial finite 1 -element countable set
{{n,n1},{n}} is non empty finite V34() countable set
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
k is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
l is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f . k is Element of the carrier of R
[n,(f . k)] is V13() non empty set
{n,(f . k)} is non empty finite countable set
{{n,(f . k)},{n}} is non empty finite V34() countable set
f . l is Element of the carrier of R
[(f . l),n1] is V13() non empty set
{(f . l),n1} is non empty finite countable set
{(f . l)} is non empty trivial finite 1 -element countable set
{{(f . l),n1},{(f . l)}} is non empty finite V34() countable set
k is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
l is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f . k is Element of the carrier of R
[n,(f . k)] is V13() non empty set
{n,(f . k)} is non empty finite countable set
{{n,(f . k)},{n}} is non empty finite V34() countable set
f . l is Element of the carrier of R
[(f . l),n1] is V13() non empty set
{(f . l),n1} is non empty finite countable set
{(f . l)} is non empty trivial finite 1 -element countable set
{{(f . l),n1},{(f . l)}} is non empty finite V34() countable set
[f9,(f . k)] is V13() non empty set
{f9,(f . k)} is non empty finite countable set
{{f9,(f . k)},{f9}} is non empty finite V34() countable set
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
k is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
l is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f . k is Element of the carrier of R
[f9,(f . k)] is V13() non empty set
{f9,(f . k)} is non empty finite countable set
{{f9,(f . k)},{f9}} is non empty finite V34() countable set
f . l is Element of the carrier of R
[(f . l),n] is V13() non empty set
{(f . l),n} is non empty finite countable set
{(f . l)} is non empty trivial finite 1 -element countable set
{{(f . l),n},{(f . l)}} is non empty finite V34() countable set
k is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
l is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f . k is Element of the carrier of R
[f9,(f . k)] is V13() non empty set
{f9,(f . k)} is non empty finite countable set
{{f9,(f . k)},{f9}} is non empty finite V34() countable set
f . l is Element of the carrier of R
[(f . l),n] is V13() non empty set
{(f . l),n} is non empty finite countable set
{(f . l)} is non empty trivial finite 1 -element countable set
{{(f . l),n},{(f . l)}} is non empty finite V34() countable set
[(f . l),n1] is V13() non empty set
{(f . l),n1} is non empty finite countable set
{{(f . l),n1},{(f . l)}} is non empty finite V34() countable set
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
b is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
a is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f . b is Element of the carrier of R
[n,(f . b)] is V13() non empty set
{n,(f . b)} is non empty finite countable set
{{n,(f . b)},{n}} is non empty finite V34() countable set
f . a is Element of the carrier of R
[(f . a),n1] is V13() non empty set
{(f . a),n1} is non empty finite countable set
{(f . a)} is non empty trivial finite 1 -element countable set
{{(f . a),n1},{(f . a)}} is non empty finite V34() countable set
b is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
a is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f . b is Element of the carrier of R
[n,(f . b)] is V13() non empty set
{n,(f . b)} is non empty finite countable set
{{n,(f . b)},{n}} is non empty finite V34() countable set
f . a is Element of the carrier of R
[(f . a),n1] is V13() non empty set
{(f . a),n1} is non empty finite countable set
{(f . a)} is non empty trivial finite 1 -element countable set
{{(f . a),n1},{(f . a)}} is non empty finite V34() countable set
[(f . l),(f . b)] is V13() non empty Element of the carrier of [:R,R:]
[:R,R:] is non empty strict RelStr
the carrier of [:R,R:] is non empty set
{(f . l),(f . b)} is non empty finite countable set
{{(f . l),(f . b)},{(f . l)}} is non empty finite V34() countable set
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
[f9,n1] is V13() non empty set
{f9,n1} is non empty finite countable set
{{f9,n1},{f9}} is non empty finite V34() countable set
(RelStr(# the carrier of R,QOE #)) is non empty strict antisymmetric RelStr
( the carrier of RelStr(# the carrier of R,QOE #), the InternalRel of RelStr(# the carrier of R,QOE #)) is Relation-like the carrier of RelStr(# the carrier of R,QOE #) -defined the carrier of RelStr(# the carrier of R,QOE #) -valued asymmetric Element of bool [: the carrier of RelStr(# the carrier of R,QOE #), the carrier of RelStr(# the carrier of R,QOE #):]
the InternalRel of RelStr(# the carrier of R,QOE #) ~ is Relation-like set
the InternalRel of RelStr(# the carrier of R,QOE #) \ ( the InternalRel of RelStr(# the carrier of R,QOE #) ~) is Relation-like the carrier of RelStr(# the carrier of R,QOE #) -defined the carrier of RelStr(# the carrier of R,QOE #) -valued Element of bool the InternalRel of RelStr(# the carrier of R,QOE #)
bool the InternalRel of RelStr(# the carrier of R,QOE #) is non empty set
RelStr(# the carrier of RelStr(# the carrier of R,QOE #),( the carrier of RelStr(# the carrier of R,QOE #), the InternalRel of RelStr(# the carrier of R,QOE #)) #) is non empty strict RelStr
the carrier of (RelStr(# the carrier of R,QOE #)) is non empty set
[:NAT, the carrier of (RelStr(# the carrier of R,QOE #)):] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of (RelStr(# the carrier of R,QOE #)):] is non empty non trivial non finite set
n is V25() V29() finite cardinal countable ext-real non negative set
n + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
n1 is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f . n1 is Element of the carrier of R
n1 + 1 is non empty V25() V29() finite cardinal countable V250() V251() ext-real positive non negative V255() V256() V267() V268() V269() V270() V271() V272() V281() V282() V283() V284() V285() Element of NAT
f . (n1 + 1) is Element of the carrier of R
f . n is Element of the carrier of R
f . (n + 1) is Element of the carrier of R
[(f . n),(f . (n + 1))] is V13() non empty Element of the carrier of [:R,R:]
[:R,R:] is non empty strict RelStr
the carrier of [:R,R:] is non empty set
{(f . n),(f . (n + 1))} is non empty finite countable set
{(f . n)} is non empty trivial finite 1 -element countable set
{{(f . n),(f . (n + 1))},{(f . n)}} is non empty finite V34() countable set
f9 is Relation-like NAT -defined the carrier of (RelStr(# the carrier of R,QOE #)) -valued Function-like non empty V19( NAT ) V20( NAT , the carrier of (RelStr(# the carrier of R,QOE #))) Element of bool [:NAT, the carrier of (RelStr(# the carrier of R,QOE #)):]
f9 . (n + 1) is Element of the carrier of (RelStr(# the carrier of R,QOE #))
f9 . n is Element of the carrier of (RelStr(# the carrier of R,QOE #))
[(f9 . (n + 1)),(f9 . (n + 1))] is V13() non empty Element of the carrier of [:(RelStr(# the carrier of R,QOE #)),(RelStr(# the carrier of R,QOE #)):]
[:(RelStr(# the carrier of R,QOE #)),(RelStr(# the carrier of R,QOE #)):] is non empty strict antisymmetric RelStr
the carrier of [:(RelStr(# the carrier of R,QOE #)),(RelStr(# the carrier of R,QOE #)):] is non empty set
{(f9 . (n + 1)),(f9 . (n + 1))} is non empty finite countable set
{(f9 . (n + 1))} is non empty trivial finite 1 -element countable set
{{(f9 . (n + 1)),(f9 . (n + 1))},{(f9 . (n + 1))}} is non empty finite V34() countable set
[(f9 . n),(f9 . n)] is V13() non empty Element of the carrier of [:(RelStr(# the carrier of R,QOE #)),(RelStr(# the carrier of R,QOE #)):]
{(f9 . n),(f9 . n)} is non empty finite countable set
{(f9 . n)} is non empty trivial finite 1 -element countable set
{{(f9 . n),(f9 . n)},{(f9 . n)}} is non empty finite V34() countable set
[(f9 . n),(f9 . (n + 1))] is V13() non empty Element of the carrier of [:(RelStr(# the carrier of R,QOE #)),(RelStr(# the carrier of R,QOE #)):]
{(f9 . n),(f9 . (n + 1))} is non empty finite countable set
{{(f9 . n),(f9 . (n + 1))},{(f9 . n)}} is non empty finite V34() countable set
k is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
l is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f . k is Element of the carrier of R
[(f9 . n),(f . k)] is V13() non empty Element of the carrier of [:(RelStr(# the carrier of R,QOE #)),R:]
[:(RelStr(# the carrier of R,QOE #)),R:] is non empty strict RelStr
the carrier of [:(RelStr(# the carrier of R,QOE #)),R:] is non empty set
{(f9 . n),(f . k)} is non empty finite countable set
{{(f9 . n),(f . k)},{(f9 . n)}} is non empty finite V34() countable set
f . l is Element of the carrier of R
[(f . l),(f9 . (n + 1))] is V13() non empty Element of the carrier of [:R,(RelStr(# the carrier of R,QOE #)):]
[:R,(RelStr(# the carrier of R,QOE #)):] is non empty strict RelStr
the carrier of [:R,(RelStr(# the carrier of R,QOE #)):] is non empty set
{(f . l),(f9 . (n + 1))} is non empty finite countable set
{(f . l)} is non empty trivial finite 1 -element countable set
{{(f . l),(f9 . (n + 1))},{(f . l)}} is non empty finite V34() countable set
l is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
k is V25() V29() finite cardinal countable V250() V251() ext-real non negative V255() V256() V267() V268() V269() V270() V271() V272() V283() V284() V285() Element of NAT
f . l is Element of the carrier of R
[(f9 . n),(f . l)] is V13() non empty Element of the carrier of [:(RelStr(# the carrier of R,QOE #)),R:]
[:(RelStr(# the carrier of R,QOE #)),R:] is non empty strict RelStr
the carrier of [:(RelStr(# the carrier of R,QOE #)),R:] is non empty set
{(f9 . n),(f . l)} is non empty finite countable set
{{(f9 . n),(f . l)},{(f9 . n)}} is non empty finite V34() countable set
f . k is Element of the carrier of R
[(f . k),(f9 . (n + 1))] is V13() non empty Element of the carrier of [:R,(RelStr(# the carrier of R,QOE #)):]
[:R,(RelStr(# the carrier of R,QOE #)):] is non empty strict RelStr
the carrier of [:R,(RelStr(# the carrier of R,QOE #)):] is non empty set
{(f . k),(f9 . (n + 1))} is non empty finite countable set
{(f . k)} is non empty trivial finite 1 -element countable set
{{(f . k),(f9 . (n + 1))},{(f . k)}} is non empty finite V34() countable set
f9 . (n1 + 1) is Element of the carrier of (RelStr(# the carrier of R,QOE #))
f9 . n1 is Element of the carrier of (RelStr(# the carrier of R,QOE #))
[(f9 . (n1 + 1)),(f9 . n1)] is V13() non empty Element of the carrier of [:(RelStr(# the carrier of R,QOE #)),(RelStr(# the carrier of R,QOE #)):]
{(f9 . (n1 + 1)),(f9 . n1)} is non empty finite countable set
{(f9 . (n1 + 1))} is non empty trivial finite 1 -element countable set
{{(f9 . (n1 + 1)),(f9 . n1)},{(f9 . (n1 + 1))}} is non empty finite V34() countable set
[(f9 . (n + 1)),(f9 . n)] is V13() non empty Element of the carrier of [:(RelStr(# the carrier of R,QOE #)),(RelStr(# the carrier of R,QOE #)):]
{(f9 . (n + 1)),(f9 . n)} is non empty finite countable set
{{(f9 . (n + 1)),(f9 . n)},{(f9 . (n + 1))}} is non empty finite V34() countable set
QOE ~ is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the InternalRel of (RelStr(# the carrier of R,QOE #)) is Relation-like the carrier of (RelStr(# the carrier of R,QOE #)) -defined the carrier of (RelStr(# the carrier of R,QOE #)) -valued Element of bool [: the carrier of (RelStr(# the carrier of R,QOE #)), the carrier of (RelStr(# the carrier of R,QOE #)):]
[: the carrier of (RelStr(# the carrier of R,QOE #)), the carrier of (RelStr(# the carrier of R,QOE #)):] is Relation-like non empty set
bool [: the carrier of (RelStr(# the carrier of R,QOE #)), the carrier of (RelStr(# the carrier of R,QOE #)):] is non empty set