REAL is non empty non trivial non finite set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty non trivial non finite set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite set
RAT is non empty non trivial non finite set
INT is non empty non trivial non finite set
{} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set
the empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of NAT
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of NAT
{{},1} is non empty finite with_finite-elements set
K266(NAT) is V83() set
[:NAT,REAL:] is non empty non trivial Relation-like non finite set
bool [:NAT,REAL:] is non empty non trivial non finite set
1 -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
[:REAL,REAL:] is non empty non trivial Relation-like non finite set
bool [:REAL,REAL:] is non empty non trivial non finite set
K662() is set
bool K662() is non empty set
K663() is Element of bool K662()
[:INT,INT:] is non empty non trivial Relation-like non finite set
bool [:INT,INT:] is non empty non trivial non finite set
[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like non finite set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial Relation-like non finite set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like non finite set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is non empty non trivial Relation-like non finite set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is non empty non trivial Relation-like non finite set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is non empty non trivial Relation-like non finite set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is non empty non trivial Relation-like non finite set
[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like non finite set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of NAT
0 is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of NAT
union {} is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
dom {} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set
rng {} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V24() V25() V26() V27() V29() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing with_non-empty_elements set
F2() is finite set
F1() is non empty finite set
{ F3(b1) where b1 is Element of F1() : P1[b1] } is set
card F2() is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
card F1() is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
{ F3(b1) where b1 is Element of F1() : b1 in F1() } is set
n is finite set
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is set
iP is Element of F1()
F3(iP) is set
cP is set
f is set
n is set
{cP} is non empty trivial finite 1 -element set
n \/ {cP} is non empty set
f \ (n \/ {cP}) is Element of bool f
bool f is non empty set
f \ n is Element of bool f
(f \ n) \ {cP} is Element of bool f
f is set
bool f is non empty set
bool (bool f) is non empty set
n is set
bool n is non empty set
bool (bool n) is non empty set
f \/ n is set
bool (f \/ n) is non empty set
bool (bool (f \/ n)) is non empty set
cP is Element of bool (bool f)
iP is Element of bool (bool n)
cP \/ iP is set
(bool f) \/ (bool n) is non empty set
f is set
n is set
f \/ n is set
cP is with_non-empty_elements a_partition of f
iP is with_non-empty_elements a_partition of n
cP \/ iP is set
bool (f \/ n) is non empty set
bool (bool (f \/ n)) is non empty set
union (cP \/ iP) is set
union cP is Element of bool f
bool f is non empty set
union iP is Element of bool n
bool n is non empty set
(union cP) \/ (union iP) is set
f \/ (union iP) is set
A is Element of bool (f \/ n)
g is Element of bool (f \/ n)
n is set
f is set
bool f is non empty set
f \ n is Element of bool f
{(f \ n)} is non empty trivial finite 1 -element Element of bool (bool f)
bool (bool f) is non empty set
cP is with_non-empty_elements a_partition of n
cP \/ {(f \ n)} is non empty set
n \/ (f \ n) is set
f is non empty non trivial non finite set
bool f is non empty non trivial non finite set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
[:NAT,f:] is non empty non trivial Relation-like non finite set
bool [:NAT,f:] is non empty non trivial non finite set
cP is non empty Relation-like NAT -defined f -valued Function-like V17( NAT ) quasi_total Element of bool [:NAT,f:]
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
Seg (n + 1) is non empty finite n + 1 -element Element of bool NAT
[:(Seg (n + 1)),f:] is non empty non trivial Relation-like non finite set
bool [:(Seg (n + 1)),f:] is non empty non trivial non finite set
cP | (Seg (n + 1)) is Relation-like NAT -defined Seg (n + 1) -defined NAT -defined f -valued Function-like finite Element of bool [:NAT,f:]
P is non empty Relation-like Seg (n + 1) -defined f -valued Function-like V17( Seg (n + 1)) quasi_total finite Element of bool [:(Seg (n + 1)),f:]
card P is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
rng P is non empty finite set
card (rng P) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
dom P is non empty finite Element of bool (Seg (n + 1))
bool (Seg (n + 1)) is non empty finite with_finite-elements set
card (dom P) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite Element of bool f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
cP is set
iP is set
[cP,iP] is non empty set
{cP,iP} is non empty finite set
{cP} is non empty trivial finite 1 -element set
{{cP,iP},{cP}} is non empty finite with_finite-elements set
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, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
[iP,cP] is non empty set
{iP,cP} is non empty finite set
{iP} is non empty trivial finite 1 -element set
{{iP,cP},{iP}} is non empty finite with_finite-elements set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
{} f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) Element of bool the carrier of f
n is set
cP is set
[n,cP] is non empty set
{n,cP} is non empty finite set
{n} is non empty trivial finite 1 -element set
{{n,cP},{n}} is non empty finite with_finite-elements set
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, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
[cP,n] is non empty set
{cP,n} is non empty finite set
{cP} is non empty trivial finite 1 -element set
{{cP,n},{cP}} is non empty finite with_finite-elements set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
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, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
iP is Element of the carrier of f
P is Element of the carrier of f
[iP,P] is non empty set
{iP,P} is non empty finite set
{iP} is non empty trivial finite 1 -element set
{{iP,P},{iP}} is non empty finite with_finite-elements set
[P,iP] is non empty set
{P,iP} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,iP},{P}} is non empty finite with_finite-elements set
iP is set
P is set
[iP,P] is non empty set
{iP,P} is non empty finite set
{iP} is non empty trivial finite 1 -element set
{{iP,P},{iP}} is non empty finite with_finite-elements set
[P,iP] is non empty set
{P,iP} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,iP},{P}} is non empty finite with_finite-elements set
P is Element of the carrier of f
A is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
{} f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) Element of bool the carrier of f
f is V139() reflexive RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued V17( the carrier of f) quasi_total reflexive Element of bool [: the carrier of f, the carrier of f:]
[: the carrier of f, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
P is set
P is set
[P,P] is non empty set
{P,P} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,P},{P}} is non empty finite with_finite-elements set
[P,P] is non empty set
{P,P} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,P},{P}} is non empty finite with_finite-elements set
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
{ the Element of the carrier of f} is non empty trivial finite 1 -element (f) Element of bool the carrier of f
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
n is Element of the carrier of f
cP is Element of the carrier of f
{n,cP} is non empty finite Element of bool the carrier of f
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
n is Element of the carrier of f
cP is Element of the carrier of f
{n,cP} is non empty finite Element of bool the carrier of f
iP is Element of the carrier of f
P is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
bool n is non empty set
cP is Element of bool n
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, the carrier of f:] is Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
P is set
P is set
[P,P] is non empty set
{P,P} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,P},{P}} is non empty finite with_finite-elements set
[P,P] is non empty set
{P,P} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,P},{P}} is non empty finite with_finite-elements set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
bool n is non empty finite with_finite-elements set
iP is finite Element of bool n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is transitive RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
cP is Element of the carrier of f
iP is Element of the carrier of f
{iP} is non empty trivial finite 1 -element set
n \/ {iP} is non empty set
P is set
P is Element of the carrier of f
A is Element of the carrier of f
f is transitive RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
cP is Element of the carrier of f
iP is Element of the carrier of f
{iP} is non empty trivial finite 1 -element set
n \/ {iP} is non empty set
P is set
P is Element of the carrier of f
A is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
cP is Element of the carrier of f
iP is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
cP is Element of the carrier of f
iP is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
{} f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
{ the Element of the carrier of f} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
n is Element of the carrier of f
cP is Element of the carrier of f
{n,cP} is non empty finite Element of bool the carrier of f
f is non empty RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
n is Element of the carrier of f
cP is Element of the carrier of f
{n,cP} is non empty finite Element of bool the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
cP is (f) Element of bool the carrier of f
iP is set
P is set
P is Element of the carrier of f
A is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
bool n is non empty set
cP is Element of bool n
iP is Element of bool the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
bool n is non empty finite with_finite-elements set
iP is finite Element of bool n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite RelStr
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of n is finite set
card the carrier of n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
{} f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
card ({} f) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
cP is finite (f) Element of bool the carrier of f
card cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
bool n is non empty set
iP is finite Element of bool n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is empty trivial finite {} -element () RelStr
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set
bool the carrier of f is non empty finite with_finite-elements set
{} f is empty trivial non proper Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
card ({} f) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of omega
n is empty trivial non proper Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
card n is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of omega
f is non empty () RelStr
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
{ the Element of the carrier of f} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
bool the carrier of f is non empty set
card { the Element of the carrier of f} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is non empty () RelStr
[#] f is non empty non proper Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is set
iP is set
f is () RelStr
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
[#] f is non proper Element of bool the carrier of f
the carrier of f is set
bool the carrier of f is non empty set
cP is Element of the carrier of f
iP is Element of the carrier of f
{cP,iP} is non empty finite set
card {cP,iP} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is RelStr
n is finite () RelStr
the carrier of n is finite set
bool the carrier of n is non empty finite with_finite-elements set
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
card the carrier of n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite (n) Element of bool the carrier of n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
{} f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
the carrier of f is set
bool the carrier of f is non empty set
card {} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite (n) Element of bool the carrier of n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is (f) Element of bool the carrier of f
bool cP is non empty set
iP is finite Element of bool cP
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is empty trivial finite {} -element () () RelStr
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set
bool the carrier of f is non empty finite with_finite-elements set
{} f is empty trivial non proper Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
card ({} f) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of omega
n is empty trivial non proper Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
card n is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of omega
f is non empty () RelStr
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of f is non empty set
the Element of the carrier of f is Element of the carrier of f
{ the Element of the carrier of f} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
bool the carrier of f is non empty set
card { the Element of the carrier of f} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is non empty () RelStr
[#] f is non empty non proper Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
(f) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is set
iP is set
f is () RelStr
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
[#] f is non proper Element of bool the carrier of f
the carrier of f is set
bool the carrier of f is non empty set
cP is Element of the carrier of f
iP is Element of the carrier of f
{cP,iP} is non empty finite set
card {cP,iP} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is RelStr
n is () () RelStr
the carrier of n is set
bool the carrier of n is non empty set
(n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
cP is finite (n) Element of bool the carrier of n
card cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite (n) Element of bool the carrier of n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
[#] n is non proper Element of bool the carrier of n
g is finite Element of bool the carrier of n
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
g is finite Element of bool the carrier of n
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
max ((n),(n)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(max ((n),(n))) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g is finite Element of bool the carrier of n
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
g \/ iP is finite Element of bool the carrier of n
(g \/ iP) \/ cP is finite Element of bool the carrier of n
e1 is finite Element of bool the carrier of n
card e1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
{ {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & ( b1 <= b2 or b2 <= b1 ) ) } is set
{ {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & not b1 <= b2 & not b2 <= b1 ) } is set
the_subsets_of_card (2,e1) is finite with_finite-elements Element of bool (bool e1)
bool e1 is non empty finite with_finite-elements set
bool (bool e1) is non empty finite with_finite-elements set
{ b1 where b1 is Element of bool e1 : card b1 = 2 } is set
{ { {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & ( b1 <= b2 or b2 <= b1 ) ) } , { {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & not b1 <= b2 & not b2 <= b1 ) } } is non empty finite set
j is set
r is Element of the carrier of n
s is Element of the carrier of n
{r,s} is non empty finite set
card j is epsilon-transitive epsilon-connected ordinal cardinal set
j is set
r is Element of the carrier of n
s is Element of the carrier of n
{r,s} is non empty finite set
card j is epsilon-transitive epsilon-connected ordinal cardinal set
j is set
r is set
s is Element of the carrier of n
Sp is Element of the carrier of n
{s,Sp} is non empty finite set
Sp is Element of the carrier of n
Sp is Element of the carrier of n
{Sp,Sp} is non empty finite set
bool (the_subsets_of_card (2,e1)) is non empty finite with_finite-elements set
j is set
union { { {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & ( b1 <= b2 or b2 <= b1 ) ) } , { {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & not b1 <= b2 & not b2 <= b1 ) } } is set
j is set
r is set
j is set
r is finite Element of bool e1
card r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
s is set
Sp is set
{s,Sp} is non empty finite set
Sp is Element of the carrier of n
Sp is Element of the carrier of n
{Sp,Sp} is non empty finite set
j is finite with_finite-elements Element of bool (the_subsets_of_card (2,e1))
r is set
s is set
Sp is Element of the carrier of n
Sp is Element of the carrier of n
{Sp,Sp} is non empty finite set
r is set
s is set
Sp is Element of the carrier of n
Sp is Element of the carrier of n
{Sp,Sp} is non empty finite set
r is finite with_finite-elements Element of bool (the_subsets_of_card (2,e1))
{ {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & ( b1 <= b2 or b2 <= b1 ) ) } /\ { {b1,b2} where b1, b2 is Element of the carrier of n : ( not b1 = b2 & b1 in e1 & b2 in e1 & not b1 <= b2 & not b2 <= b1 ) } is set
s is set
Sp is Element of the carrier of n
Sp is Element of the carrier of n
{Sp,Sp} is non empty finite set
Sp is Element of the carrier of n
cc is Element of the carrier of n
{Sp,cc} is non empty finite set
j is finite with_finite-elements with_non-empty_elements a_partition of the_subsets_of_card (2,e1)
card j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
r is finite Element of bool e1
card r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
s is finite Element of bool the carrier of n
card s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
the_subsets_of_card (2,s) is finite with_finite-elements Element of bool (bool s)
bool s is non empty finite with_finite-elements set
bool (bool s) is non empty finite with_finite-elements set
{ b1 where b1 is Element of bool s : card b1 = 2 } is set
Sp is finite Element of j
Sp is Element of the carrier of n
Sp is Element of the carrier of n
{Sp,Sp} is non empty finite set
card {Sp,Sp} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cc is Element of the carrier of n
d is Element of the carrier of n
{cc,d} is non empty finite set
Sp is Element of the carrier of n
Sp is Element of the carrier of n
{Sp,Sp} is non empty finite set
card {Sp,Sp} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cc is Element of the carrier of n
d is Element of the carrier of n
{cc,d} is non empty finite set
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
downarrow n is Element of bool the carrier of f
n \/ (downarrow n) is Element of bool the carrier of f
uparrow n is Element of bool the carrier of f
n \/ (uparrow n) is Element of bool the carrier of f
f is transitive antisymmetric RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
uparrow n is Element of bool the carrier of f
n \/ (uparrow n) is Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
downarrow n is Element of bool the carrier of f
n \/ (downarrow n) is Element of bool the carrier of f
cP is set
iP is Element of the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f
A is Element of the carrier of f
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
[#] f is non proper Element of bool the carrier of f
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(f,n) is Element of bool the carrier of f
uparrow n is Element of bool the carrier of f
n \/ (uparrow n) is Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
downarrow n is Element of bool the carrier of f
n \/ (downarrow n) is Element of bool the carrier of f
(f,n) \/ (f,n) is Element of bool the carrier of f
iP is set
P is Element of the carrier of f
{P} is non empty trivial finite 1 -element set
n \/ {P} is non empty finite set
A is Element of the carrier of f
g is Element of the carrier of f
card (n \/ {P}) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(card n) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
f is transitive RelStr
the carrier of f is set
bool the carrier of f is non empty set
[#] f is non proper Element of bool the carrier of f
n is Element of the carrier of f
cP is Element of bool the carrier of f
(f,cP) is Element of bool the carrier of f
downarrow cP is Element of bool the carrier of f
cP \/ (downarrow cP) is Element of bool the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f
f is transitive RelStr
the carrier of f is set
bool the carrier of f is non empty set
[#] f is non proper Element of bool the carrier of f
n is Element of the carrier of f
cP is Element of bool the carrier of f
(f,cP) is Element of bool the carrier of f
uparrow cP is Element of bool the carrier of f
cP \/ (uparrow cP) is Element of bool the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
[#] f is non proper Element of bool the carrier of f
cP is set
iP is set
iP is Element of bool the carrier of f
P is Element of the carrier of f
P is Element of bool the carrier of f
A is Element of the carrier of f
iP is Element of bool the carrier of f
P is Element of bool the carrier of f
iP is Element of bool the carrier of f
P is Element of bool the carrier of f
cP is Element of bool the carrier of f
iP is Element of bool the carrier of f
P is set
P is Element of the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f
A is Element of the carrier of f
g is Element of the carrier of f
cP is set
iP is set
iP is Element of bool the carrier of f
P is Element of the carrier of f
P is Element of bool the carrier of f
A is Element of the carrier of f
iP is Element of bool the carrier of f
P is Element of bool the carrier of f
iP is Element of bool the carrier of f
P is Element of bool the carrier of f
cP is Element of bool the carrier of f
iP is Element of bool the carrier of f
P is set
P is Element of the carrier of f
P is Element of the carrier of f
P is Element of the carrier of f
A is Element of the carrier of f
g is Element of the carrier of f
f is non empty transitive antisymmetric () RelStr
(f) is Element of bool the carrier of f
the carrier of f is non empty set
bool the carrier of f is non empty set
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, the carrier of f:] is non empty Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
the Element of the carrier of f is Element of the carrier of f
{ the Element of the carrier of f} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
card { the Element of the carrier of f} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is Element of the carrier of f
[#] f is non empty non proper Element of bool the carrier of f
P is Element of the carrier of f
{P} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
iP \/ {P} is non empty finite Element of bool the carrier of f
g is finite (f) Element of bool the carrier of f
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(card iP) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(card iP) + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(f) is Element of bool the carrier of f
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, the carrier of f:] is non empty Relation-like set
bool [: the carrier of f, the carrier of f:] is non empty set
iP is finite (f) Element of bool the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
the Element of the carrier of f is Element of the carrier of f
{ the Element of the carrier of f} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
card { the Element of the carrier of f} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is Element of the carrier of f
[#] f is non empty non proper Element of bool the carrier of f
P is Element of the carrier of f
{P} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
iP \/ {P} is non empty finite Element of bool the carrier of f
g is finite (f) Element of bool the carrier of f
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(card iP) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(card iP) + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
f is RelStr
(f) is Element of bool the carrier of f
the carrier of f is set
bool the carrier of f is non empty set
cP is Element of the carrier of f
iP is Element of the carrier of f
[#] f is non proper Element of bool the carrier of f
(f) is Element of bool the carrier of f
cP is Element of the carrier of f
iP is Element of the carrier of f
[#] f is non proper Element of bool the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is (f) Element of bool the carrier of f
n is (f) Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
uparrow n is Element of bool the carrier of f
n \/ (uparrow n) is Element of bool the carrier of f
cP is set
[#] f is non proper Element of bool the carrier of f
iP is Element of the carrier of f
P is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is (f) Element of bool the carrier of f
n is (f) Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
downarrow n is Element of bool the carrier of f
n \/ (downarrow n) is Element of bool the carrier of f
cP is set
[#] f is non proper Element of bool the carrier of f
iP is Element of the carrier of f
P is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
cP is ( subrelstr n) Element of bool the carrier of (subrelstr n)
iP is Element of the carrier of f
P is Element of the carrier of f
P is Element of the carrier of (subrelstr n)
A is Element of the carrier of (subrelstr n)
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
cP is (f) Element of bool the carrier of f
cP /\ n is Element of bool the carrier of f
P is Element of the carrier of (subrelstr n)
A is Element of the carrier of (subrelstr n)
g is Element of the carrier of f
g is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
cP is ( subrelstr n) Element of bool the carrier of (subrelstr n)
{} f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
{} f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected (f) (f) Element of bool the carrier of f
P is Element of bool the carrier of f
P is Element of the carrier of f
A is Element of the carrier of f
g is Element of the carrier of (subrelstr n)
g is Element of the carrier of (subrelstr n)
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
cP is (f) Element of bool the carrier of f
cP /\ n is Element of bool the carrier of f
{} (subrelstr n) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected ( subrelstr n) ( subrelstr n) Element of bool the carrier of (subrelstr n)
{} (subrelstr n) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected ( subrelstr n) ( subrelstr n) Element of bool the carrier of (subrelstr n)
P is Element of bool the carrier of (subrelstr n)
A is Element of the carrier of (subrelstr n)
g is Element of the carrier of (subrelstr n)
g is Element of the carrier of f
g is Element of the carrier of f
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
cP is Element of bool the carrier of (subrelstr n)
iP is Element of the carrier of (subrelstr n)
P is Element of the carrier of f
P is Element of the carrier of f
A is Element of the carrier of (subrelstr n)
f is RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
cP is Element of bool the carrier of (subrelstr n)
iP is Element of the carrier of (subrelstr n)
P is Element of the carrier of f
P is Element of the carrier of f
A is Element of the carrier of (subrelstr n)
f is transitive RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
downarrow n is Element of bool the carrier of f
n \/ (downarrow n) is Element of bool the carrier of f
subrelstr (f,n) is strict transitive V147(f) SubRelStr of f
the carrier of (subrelstr (f,n)) is set
bool the carrier of (subrelstr (f,n)) is non empty set
cP is ( subrelstr (f,n)) Element of bool the carrier of (subrelstr (f,n))
iP is Element of the carrier of f
P is Element of the carrier of f
g is Element of the carrier of (subrelstr (f,n))
g is Element of the carrier of f
A is Element of the carrier of (subrelstr (f,n))
A is Element of the carrier of (subrelstr (f,n))
A is Element of the carrier of (subrelstr (f,n))
f is transitive RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is (f) Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
uparrow n is Element of bool the carrier of f
n \/ (uparrow n) is Element of bool the carrier of f
subrelstr (f,n) is strict transitive V147(f) SubRelStr of f
the carrier of (subrelstr (f,n)) is set
bool the carrier of (subrelstr (f,n)) is non empty set
cP is ( subrelstr (f,n)) Element of bool the carrier of (subrelstr (f,n))
iP is Element of the carrier of f
P is Element of the carrier of f
g is Element of the carrier of (subrelstr (f,n))
g is Element of the carrier of f
A is Element of the carrier of (subrelstr (f,n))
A is Element of the carrier of (subrelstr (f,n))
A is Element of the carrier of (subrelstr (f,n))
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
cP is finite (f) Element of bool the carrier of f
card cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
{} (subrelstr n) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected ( subrelstr n) ( subrelstr n) Element of bool the carrier of (subrelstr n)
card ({} (subrelstr n)) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of omega
P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
A is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) SubRelStr of f
cP is finite (f) Element of bool the carrier of f
card cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
{} (subrelstr n) is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing strongly_connected ( subrelstr n) ( subrelstr n) Element of bool the carrier of (subrelstr n)
iP is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
A is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
g is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is non empty transitive antisymmetric () RelStr
the carrier of f is non empty set
[#] f is non empty non proper Element of bool the carrier of f
bool the carrier of f is non empty set
n is Element of the carrier of f
{n} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
(f,{n}) is Element of bool the carrier of f
downarrow {n} is Element of bool the carrier of f
{n} \/ (downarrow {n}) is non empty Element of bool the carrier of f
subrelstr (f,{n}) is strict transitive antisymmetric V147(f) () SubRelStr of f
P is non empty transitive antisymmetric () RelStr
(P) is non empty (P) Element of bool the carrier of P
the carrier of P is non empty set
bool the carrier of P is non empty set
P is set
[#] P is non empty non proper Element of bool the carrier of P
A is Element of the carrier of P
g is Element of the carrier of f
downarrow n is Element of bool the carrier of f
f is transitive antisymmetric () RelStr
(f) is (f) Element of bool the carrier of f
the carrier of f is set
bool the carrier of f is non empty set
(f,(f)) is Element of bool the carrier of f
uparrow (f) is Element of bool the carrier of f
(f) \/ (uparrow (f)) is Element of bool the carrier of f
[#] f is non proper Element of bool the carrier of f
iP is set
P is Element of the carrier of f
P is Element of the carrier of f
f is non empty transitive antisymmetric () RelStr
the carrier of f is non empty set
[#] f is non empty non proper Element of bool the carrier of f
bool the carrier of f is non empty set
n is Element of the carrier of f
{n} is non empty trivial finite 1 -element (f) (f) Element of bool the carrier of f
(f,{n}) is Element of bool the carrier of f
uparrow {n} is Element of bool the carrier of f
{n} \/ (uparrow {n}) is non empty Element of bool the carrier of f
subrelstr (f,{n}) is strict transitive antisymmetric V147(f) () SubRelStr of f
P is non empty transitive antisymmetric () RelStr
(P) is non empty (P) Element of bool the carrier of P
the carrier of P is non empty set
bool the carrier of P is non empty set
P is set
[#] P is non empty non proper Element of bool the carrier of P
A is Element of the carrier of P
g is Element of the carrier of f
uparrow n is Element of bool the carrier of f
f is transitive antisymmetric () RelStr
(f) is (f) Element of bool the carrier of f
the carrier of f is set
bool the carrier of f is non empty set
(f,(f)) is Element of bool the carrier of f
downarrow (f) is Element of bool the carrier of f
(f) \/ (downarrow (f)) is Element of bool the carrier of f
[#] f is non proper Element of bool the carrier of f
iP is set
P is Element of the carrier of f
P is Element of the carrier of f
f is transitive antisymmetric () RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is (f) Element of bool the carrier of f
n is (f) Element of bool the carrier of f
cP is set
[#] f is non proper Element of bool the carrier of f
iP is Element of the carrier of f
P is Element of the carrier of f
f is transitive antisymmetric () RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is (f) Element of bool the carrier of f
n is (f) Element of bool the carrier of f
cP is set
[#] f is non proper Element of bool the carrier of f
iP is Element of the carrier of f
P is Element of the carrier of f
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) () SubRelStr of f
((subrelstr n)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
iP is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is Element of bool the carrier of f
subrelstr cP is strict V147(f) () SubRelStr of f
((subrelstr cP)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n /\ cP is finite Element of bool the carrier of f
the carrier of (subrelstr cP) is set
bool the carrier of (subrelstr cP) is non empty set
iP is finite ( subrelstr cP) Element of bool the carrier of (subrelstr cP)
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is Element of bool the carrier of f
subrelstr n is strict V147(f) () SubRelStr of f
((subrelstr n)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of (subrelstr n) is set
bool the carrier of (subrelstr n) is non empty set
cP is finite ( subrelstr n) Element of bool the carrier of (subrelstr n)
card cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is Element of bool the carrier of f
subrelstr cP is strict V147(f) () SubRelStr of f
((subrelstr cP)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n /\ cP is finite Element of bool the carrier of f
the carrier of (subrelstr cP) is set
bool the carrier of (subrelstr cP) is non empty set
iP is finite ( subrelstr cP) Element of bool the carrier of (subrelstr cP)
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is RelStr
the carrier of f is set
f is RelStr
the carrier of f is set
cP is with_non-empty_elements a_partition of the carrier of f
bool the carrier of f is non empty set
iP is set
SmallestPartition the carrier of f is with_non-empty_elements a_partition of the carrier of f
cP is with_non-empty_elements a_partition of the carrier of f
iP is set
bool the carrier of f is non empty set
{ {b1} where b1 is Element of the carrier of f : verum } is set
P is Element of the carrier of f
{P} is non empty trivial finite 1 -element set
f is empty trivial finite {} -element () () RelStr
the carrier of f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set
n is finite with_finite-elements with_non-empty_elements a_partition of the carrier of f
cP is set
bool the carrier of f is non empty finite with_finite-elements set
f is finite () () RelStr
the carrier of f is finite set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is finite with_finite-elements with_non-empty_elements (f) a_partition of the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
bool the carrier of f is non empty finite with_finite-elements set
cP is finite (f) Element of bool the carrier of f
card cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
card (card n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
card (card cP) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is set
P is Element of the carrier of f
union n is finite Element of bool the carrier of f
A is set
[:cP,n:] is Relation-like finite set
bool [:cP,n:] is non empty finite with_finite-elements set
P is Relation-like cP -defined n -valued Function-like quasi_total finite Element of bool [:cP,n:]
P is set
A is set
P . P is set
P . A is set
f is () RelStr
the carrier of f is set
bool the carrier of f is non empty set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is with_non-empty_elements (f) a_partition of the carrier of f
card cP is epsilon-transitive epsilon-connected ordinal cardinal set
[:n,cP:] is Relation-like set
bool [:n,cP:] is non empty set
the Relation-like n -defined cP -valued Function-like quasi_total finite Element of bool [:n,cP:] is Relation-like n -defined cP -valued Function-like quasi_total finite Element of bool [:n,cP:]
dom the Relation-like n -defined cP -valued Function-like quasi_total finite Element of bool [:n,cP:] is finite Element of bool n
bool n is non empty finite with_finite-elements set
P is Relation-like n -defined cP -valued Function-like quasi_total finite Element of bool [:n,cP:]
A is set
P . A is set
P is set
P is Element of the carrier of f
union cP is Element of bool the carrier of f
A is set
P is Relation-like n -defined cP -valued Function-like quasi_total finite Element of bool [:n,cP:]
P is set
dom P is finite set
A is set
P . P is set
P . A is set
dom P is finite Element of bool n
bool n is non empty finite with_finite-elements set
rng P is finite set
P is set
P . P is set
f is finite () () RelStr
the carrier of f is finite set
bool the carrier of f is non empty finite with_finite-elements set
n is finite (f) Element of bool the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is finite with_finite-elements with_non-empty_elements (f) a_partition of the carrier of f
card cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
[:n,cP:] is Relation-like finite set
bool [:n,cP:] is non empty finite with_finite-elements set
iP is Relation-like n -defined cP -valued Function-like quasi_total finite Element of bool [:n,cP:]
P is set
P /\ n is finite Element of bool the carrier of f
rng iP is finite set
dom iP is finite Element of bool n
bool n is non empty finite with_finite-elements set
P is set
iP . P is set
A is Element of n
{A} is non empty trivial finite 1 -element set
g is set
f is non empty transitive antisymmetric () RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
(f) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is finite (f) Element of bool the carrier of f
(f,n) is Element of bool the carrier of f
uparrow n is Element of bool the carrier of f
n \/ (uparrow n) is Element of bool the carrier of f
subrelstr (f,n) is strict transitive antisymmetric V147(f) () SubRelStr of f
the carrier of (subrelstr (f,n)) is set
(f,n) is Element of bool the carrier of f
downarrow n is Element of bool the carrier of f
n \/ (downarrow n) is Element of bool the carrier of f
subrelstr (f,n) is strict transitive antisymmetric V147(f) () SubRelStr of f
the carrier of (subrelstr (f,n)) is set
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
cP is with_non-empty_elements ( subrelstr (f,n)) a_partition of the carrier of (subrelstr (f,n))
card cP is epsilon-transitive epsilon-connected ordinal cardinal set
iP is with_non-empty_elements ( subrelstr (f,n)) a_partition of the carrier of (subrelstr (f,n))
card iP is epsilon-transitive epsilon-connected ordinal cardinal set
n /\ (f,n) is finite Element of bool the carrier of f
g is non empty transitive antisymmetric () RelStr
the carrier of g is non empty set
bool the carrier of g is non empty set
[:n,cP:] is Relation-like set
bool [:n,cP:] is non empty set
g is Relation-like n -defined cP -valued Function-like quasi_total finite Element of bool [:n,cP:]
dom g is finite Element of bool n
bool n is non empty finite with_finite-elements set
rng g is finite set
n /\ (f,n) is finite Element of bool the carrier of f
g is non empty transitive antisymmetric () RelStr
the carrier of g is non empty set
bool the carrier of g is non empty set
[:n,iP:] is Relation-like set
bool [:n,iP:] is non empty set
e1 is Relation-like n -defined iP -valued Function-like quasi_total finite Element of bool [:n,iP:]
dom e1 is finite Element of bool n
rng e1 is finite set
g .\/ e1 is Relation-like Function-like set
rng (g .\/ e1) is set
dom (g .\/ e1) is set
(dom g) \/ (dom e1) is finite Element of bool n
p2 is set
i is set
(g .\/ e1) . i is set
g . i is set
e1 . i is set
(g . i) \/ (e1 . i) is set
union (rng (g .\/ e1)) is set
p2 is set
i is set
j is set
(g .\/ e1) . j is set
g . j is set
e1 . j is set
(g . j) \/ (e1 . j) is set
[#] f is non empty non proper Element of bool the carrier of f
(f,n) \/ (f,n) is Element of bool the carrier of f
union cP is Element of bool the carrier of (subrelstr (f,n))
bool the carrier of (subrelstr (f,n)) is non empty set
i is set
j is set
g . j is set
(g .\/ e1) . j is set
e1 . j is set
(g . j) \/ (e1 . j) is set
union iP is Element of bool the carrier of (subrelstr (f,n))
bool the carrier of (subrelstr (f,n)) is non empty set
i is set
j is set
e1 . j is set
(g .\/ e1) . j is set
g . j is set
(g . j) \/ (e1 . j) is set
p2 is Element of bool the carrier of f
i is set
(g .\/ e1) . i is set
g . i is set
e1 . i is set
(g . i) \/ (e1 . i) is set
s is Element of bool the carrier of g
Sp is Element of bool the carrier of f
Sp is set
(g .\/ e1) . Sp is set
g . Sp is set
e1 . Sp is set
(g . Sp) \/ (e1 . Sp) is set
dd is Element of bool the carrier of g
Sp is Element of bool the carrier of g
x is Element of bool the carrier of g
p2 /\ Sp is Element of bool the carrier of f
z is set
g . z is set
e1 . z is set
s /\ dd is Element of bool the carrier of g
cfz is Element of bool the carrier of g
s /\ cfz is Element of bool the carrier of g
cgz is Element of bool the carrier of g
cgz /\ x is Element of bool the carrier of g
cfz is Element of bool the carrier of g
dd /\ cfz is Element of bool the carrier of g
cgz is Element of bool the carrier of g
cgz /\ Sp is Element of bool the carrier of g
Sp /\ x is Element of bool the carrier of g
p2 is set
i is set
(g .\/ e1) . i is set
g . i is set
e1 . i is set
(g . i) \/ (e1 . i) is set
Sp is Element of the carrier of f
s is Element of bool the carrier of f
Sp is Element of the carrier of f
Sp is Element of the carrier of f
g . Sp is set
Sp is Element of the carrier of f
g . Sp is set
e1 . Sp is set
Sp is Element of the carrier of f
e1 . Sp is set
g . Sp is set
Sp is Element of the carrier of f
e1 . Sp is set
Sp is Element of the carrier of f
g . Sp is set
e1 . Sp is set
p2 is set
i is set
(g .\/ e1) . p2 is set
(g .\/ e1) . i is set
g . p2 is set
e1 . p2 is set
(g . p2) \/ (e1 . p2) is set
g . i is set
e1 . i is set
(g . i) \/ (e1 . i) is set
p2 is non empty with_non-empty_elements (f) a_partition of the carrier of f
card p2 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card (g .\/ e1) is epsilon-transitive epsilon-connected ordinal cardinal set
f is RelStr
the carrier of f is set
f is RelStr
the carrier of f is set
cP is with_non-empty_elements a_partition of the carrier of f
iP is set
bool the carrier of f is non empty set
SmallestPartition the carrier of f is with_non-empty_elements a_partition of the carrier of f
iP is with_non-empty_elements a_partition of the carrier of f
P is set
bool the carrier of f is non empty set
{ {b1} where b1 is Element of the carrier of f : verum } is set
cP is non empty RelStr
the carrier of cP is non empty set
P is Element of the carrier of cP
{P} is non empty trivial finite 1 -element (cP) (cP) Element of bool the carrier of cP
bool the carrier of cP is non empty set
f is empty trivial finite {} -element () () RelStr
the carrier of f is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding with_finite-elements cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() real V51() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set
n is finite with_finite-elements with_non-empty_elements a_partition of the carrier of f
cP is set
bool the carrier of f is non empty finite with_finite-elements set
f is finite () () RelStr
the carrier of f is finite set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is finite with_finite-elements with_non-empty_elements (f) a_partition of the carrier of f
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
bool the carrier of f is non empty finite with_finite-elements set
cP is finite (f) Element of bool the carrier of f
card cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
card (card n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
card (card cP) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is set
P is Element of the carrier of f
union n is finite Element of bool the carrier of f
A is set
[:cP,n:] is Relation-like finite set
bool [:cP,n:] is non empty finite with_finite-elements set
P is Relation-like cP -defined n -valued Function-like quasi_total finite Element of bool [:cP,n:]
P is set
A is set
P . P is set
P . A is set
f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is finite transitive antisymmetric () () RelStr
card n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of n is finite set
card the carrier of n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite with_finite-elements with_non-empty_elements (n) a_partition of the carrier of n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
bool the carrier of n is non empty finite with_finite-elements set
(n) is finite (n) Element of bool the carrier of n
(n) is finite (n) Element of bool the carrier of n
iP is finite (n) Element of bool the carrier of n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
iP is finite (n) Element of bool the carrier of n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(n,iP) is finite Element of bool the carrier of n
uparrow iP is finite Element of bool the carrier of n
iP \/ (uparrow iP) is finite Element of bool the carrier of n
(n,iP) is finite Element of bool the carrier of n
downarrow iP is finite Element of bool the carrier of n
iP \/ (downarrow iP) is finite Element of bool the carrier of n
subrelstr (n,iP) is finite strict transitive antisymmetric V147(n) () () SubRelStr of n
subrelstr (n,iP) is finite strict transitive antisymmetric V147(n) () () SubRelStr of n
the carrier of (subrelstr (n,iP)) is finite set
the carrier of (subrelstr (n,iP)) is finite set
g is non empty finite transitive antisymmetric () () RelStr
(g) is non empty finite (g) Element of bool the carrier of g
the carrier of g is non empty finite set
bool the carrier of g is non empty finite with_finite-elements set
g is set
(g) is non empty finite (g) Element of bool the carrier of g
g is set
e1 is finite transitive antisymmetric () () RelStr
card e1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of e1 is finite set
card the carrier of e1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(e1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
e2 is finite with_finite-elements with_non-empty_elements (e1) a_partition of the carrier of e1
card e2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
p1 is finite transitive antisymmetric () () RelStr
card p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of p1 is finite set
card the carrier of p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(p1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
p2 is finite with_finite-elements with_non-empty_elements (p1) a_partition of the carrier of p1
card p2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(g) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
i is finite with_finite-elements with_non-empty_elements (n) a_partition of the carrier of n
card i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
bool the carrier of n is non empty finite with_finite-elements set
(n) is finite (n) Element of bool the carrier of n
(n) is finite (n) Element of bool the carrier of n
iP is finite (n) Element of bool the carrier of n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is non empty finite transitive antisymmetric () () RelStr
the carrier of P is non empty finite set
the Element of (n) is Element of (n)
(P) is non empty finite (P) Element of bool the carrier of P
bool the carrier of P is non empty finite with_finite-elements set
[#] P is non empty non proper finite Element of bool the carrier of P
g is Element of the carrier of P
g is Element of the carrier of P
{g,g} is non empty finite Element of bool the carrier of P
the carrier of n \ {g,g} is finite Element of bool the carrier of n
( the carrier of n \ {g,g}) \/ {g,g} is non empty finite set
the carrier of n \ ( the carrier of n \ {g,g}) is finite Element of bool the carrier of n
e1 is finite Element of bool the carrier of P
subrelstr e1 is finite strict transitive antisymmetric V147(P) () () SubRelStr of P
the carrier of (subrelstr e1) is finite set
card e1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
card (subrelstr e1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
card the carrier of (subrelstr e1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
card the carrier of n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
card {g,g} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(card the carrier of n) - (card {g,g}) is ext-real V49() real V51() set
((subrelstr e1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
p1 is finite with_finite-elements with_non-empty_elements ( subrelstr e1) a_partition of the carrier of (subrelstr e1)
card p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(P) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(P) - 1 is ext-real V49() real V51() set
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(0 + 1) - 1 is ext-real V49() real V51() set
iP /\ e1 is finite Element of bool the carrier of P
iP /\ the carrier of n is finite Element of bool the carrier of n
iP \ {g,g} is finite Element of bool the carrier of n
{g} is non empty trivial finite 1 -element (P) (P) Element of bool the carrier of P
{g} is non empty trivial finite 1 -element (P) (P) Element of bool the carrier of P
{g} \/ {g} is non empty finite Element of bool the carrier of P
bool the carrier of (subrelstr e1) is non empty finite with_finite-elements set
s is finite ( subrelstr e1) Element of bool the carrier of (subrelstr e1)
card s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP \ {g} is finite Element of bool the carrier of n
card {g} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(card iP) - (card {g}) is ext-real V49() real V51() set
(P) is non empty finite (P) Element of bool the carrier of P
iP \ {g} is finite Element of bool the carrier of n
card {g} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(card iP) - (card {g}) is ext-real V49() real V51() set
(P) is non empty finite (P) Element of bool the carrier of P
Sp is finite ( subrelstr e1) Element of bool the carrier of (subrelstr e1)
card Sp is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(card s) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
Sp is finite ( subrelstr e1) Element of bool the carrier of (subrelstr e1)
card Sp is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
((subrelstr e1)) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
((P) - 1) + 1 is ext-real V49() real V51() set
{{g,g}} is non empty trivial finite with_finite-elements 1 -element Element of bool (bool the carrier of P)
bool (bool the carrier of P) is non empty finite with_finite-elements set
p1 \/ {{g,g}} is non empty finite with_finite-elements set
Sp is set
Sp is finite with_finite-elements with_non-empty_elements (n) a_partition of the carrier of n
card Sp is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
bool the carrier of n is non empty finite with_finite-elements set
(n) is finite (n) Element of bool the carrier of n
(n) is finite (n) Element of bool the carrier of n
iP is finite (n) Element of bool the carrier of n
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
f is finite transitive antisymmetric () () RelStr
the carrier of f is finite set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
card f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
card the carrier of f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
f is non empty () RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
f is non empty () RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
cP is Element of the carrier of f
iP is Element of the carrier of f
{cP,iP} is non empty finite Element of bool the carrier of f
P is non empty finite Element of bool the carrier of f
subrelstr P is non empty finite strict V147(f) () () SubRelStr of f
the carrier of (subrelstr P) is non empty finite set
(f) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
P /\ n is finite Element of bool the carrier of f
A is non empty finite with_finite-elements with_non-empty_elements ( subrelstr P) a_partition of the carrier of (subrelstr P)
card A is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
g is set
g is set
bool the carrier of (subrelstr P) is non empty finite with_finite-elements set
f is non empty transitive antisymmetric () RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
n is Element of bool the carrier of f
cP is set
{cP} is non empty trivial finite 1 -element set
iP is non empty finite Element of bool the carrier of f
subrelstr iP is non empty finite strict transitive antisymmetric V147(f) () () SubRelStr of f
the carrier of (subrelstr iP) is non empty finite set
(f) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP /\ n is finite Element of bool the carrier of f
((subrelstr iP)) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
P is non empty finite with_finite-elements with_non-empty_elements ( subrelstr iP) a_partition of the carrier of (subrelstr iP)
card P is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
union P is finite Element of bool the carrier of (subrelstr iP)
bool the carrier of (subrelstr iP) is non empty finite with_finite-elements set
P is set
A is set
A is set
n /\ A is Element of bool the carrier of f
g is set
bool iP is non empty finite with_finite-elements set
g is finite Element of bool iP
g is finite Element of bool iP
g /\ g is finite Element of bool iP
bool the carrier of (subrelstr iP) is non empty finite with_finite-elements set
the finite Element of P is finite Element of P
A is set
n /\ A is Element of bool the carrier of f
f is non empty transitive antisymmetric () RelStr
the carrier of f is non empty set
bool the carrier of f is non empty set
{ b1 where b1 is Element of bool the carrier of f : b1 is (f) } is set
the Element of the carrier of f is Element of the carrier of f
{ the Element of the carrier of f} is non empty trivial finite 1 -element (f) (f) (f) Element of bool the carrier of f
iP is set
union iP is set
A is set
g is Element of bool the carrier of f
P is set
A is Element of bool the carrier of f
g is non empty finite Element of bool the carrier of f
subrelstr g is non empty finite strict transitive antisymmetric V147(f) () () SubRelStr of f
the carrier of (subrelstr g) is non empty finite set
(f) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g /\ A is finite Element of bool the carrier of f
g /\ P is finite Element of bool the carrier of f
((subrelstr g)) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g is non empty finite with_finite-elements with_non-empty_elements ( subrelstr g) a_partition of the carrier of (subrelstr g)
card g is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
bool the carrier of (subrelstr g) is non empty finite with_finite-elements set
the finite Element of g is finite Element of g
g is set
A /\ g is Element of bool the carrier of f
g is set
g is set
[:(g /\ P),iP:] is Relation-like set
bool [:(g /\ P),iP:] is non empty set
g is Relation-like g /\ P -defined iP -valued Function-like quasi_total finite Element of bool [:(g /\ P),iP:]
rng g is finite set
g is set
e1 is Element of bool the carrier of f
e2 is set
g . e2 is set
g /\ e1 is finite Element of bool the carrier of f
e2 is non empty finite with_finite-elements with_non-empty_elements ( subrelstr g) a_partition of the carrier of (subrelstr g)
card e2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
p1 is set
p1 is set
p2 is set
p2 is set
A /\ p2 is Element of bool the carrier of f
i is set
bool g is non empty finite with_finite-elements set
e1 /\ p2 is Element of bool the carrier of f
g is set
iP is set
P is Element of bool the carrier of f
P is non empty Element of bool the carrier of f
A is Element of bool the carrier of f
f is transitive antisymmetric () RelStr
the carrier of f is set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is non empty transitive antisymmetric () RelStr
(n) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of n is non empty set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
cP is non empty transitive antisymmetric () RelStr
(cP) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of cP is non empty set
bool the carrier of cP is non empty set
iP is non empty Element of bool the carrier of cP
{iP} is non empty trivial finite 1 -element Element of bool (bool the carrier of cP)
bool (bool the carrier of cP) is non empty set
P is set
P is non empty with_non-empty_elements (cP) a_partition of the carrier of cP
card P is non empty epsilon-transitive epsilon-connected ordinal cardinal set
[#] cP is non empty non proper Element of bool the carrier of cP
the carrier of cP \ iP is Element of bool the carrier of cP
the carrier of cP \ ( the carrier of cP \ iP) is Element of bool the carrier of cP
the carrier of cP /\ iP is Element of bool the carrier of cP
A is Element of bool the carrier of cP
subrelstr A is strict transitive antisymmetric V147(cP) () SubRelStr of cP
g is non empty transitive antisymmetric () RelStr
the carrier of g is non empty set
(g) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
bool the carrier of g is non empty set
g is finite (g) Element of bool the carrier of g
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
g is set
{g} is non empty trivial finite 1 -element set
iP \/ {g} is non empty set
g is Element of bool the carrier of cP
e1 is non empty finite Element of bool the carrier of cP
subrelstr e1 is non empty finite strict transitive antisymmetric V147(cP) () () SubRelStr of cP
the carrier of (subrelstr e1) is non empty finite set
e1 /\ g is finite set
e1 /\ (iP \/ {g}) is finite set
e1 /\ iP is finite Element of bool the carrier of cP
e1 /\ g is finite Element of bool the carrier of cP
e2 is set
e2 is set
e1 /\ iP is finite set
e2 is non empty finite with_finite-elements with_non-empty_elements ( subrelstr e1) a_partition of the carrier of (subrelstr e1)
card e2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
p1 is set
p1 is set
p2 is set
g /\ p2 is Element of bool the carrier of cP
i is set
iP /\ p2 is Element of bool the carrier of cP
e2 is non empty finite with_finite-elements with_non-empty_elements ( subrelstr e1) a_partition of the carrier of (subrelstr e1)
card e2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
p1 is set
g is Relation-like Function-like set
dom g is set
rng g is set
union (rng g) is set
e1 is set
e2 is set
g . e2 is set
{e2} is non empty trivial finite 1 -element set
iP \/ {e2} is non empty set
p1 is non empty finite Element of bool the carrier of cP
subrelstr p1 is non empty finite strict transitive antisymmetric V147(cP) () () SubRelStr of cP
the carrier of (subrelstr p1) is non empty finite set
p1 /\ (iP \/ {e2}) is finite set
e1 is set
e2 is set
p1 is set
g . p1 is set
{p1} is non empty trivial finite 1 -element set
iP \/ {p1} is non empty set
p2 is non empty finite Element of bool the carrier of cP
subrelstr p2 is non empty finite strict transitive antisymmetric V147(cP) () () SubRelStr of cP
the carrier of (subrelstr p2) is non empty finite set
p2 /\ (iP \/ {p1}) is finite set
g is non empty finite (cP) Element of bool the carrier of cP
e1 is set
g . e1 is set
{e1} is non empty trivial finite 1 -element set
iP \/ {e1} is non empty set
e2 is non empty finite Element of bool the carrier of cP
subrelstr e2 is non empty finite strict transitive antisymmetric V147(cP) () () SubRelStr of cP
the carrier of (subrelstr e2) is non empty finite set
e2 /\ (iP \/ {e1}) is finite set
e1 is non empty finite Element of bool the carrier of cP
subrelstr e1 is non empty finite strict transitive antisymmetric V147(cP) () () SubRelStr of cP
the carrier of (subrelstr e1) is non empty finite set
e1 /\ iP is finite set
p1 is non empty finite with_finite-elements with_non-empty_elements ( subrelstr e1) a_partition of the carrier of (subrelstr e1)
card p1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
e1 /\ iP is finite Element of bool the carrier of cP
p2 is set
p2 is set
bool the carrier of (subrelstr e1) is non empty finite with_finite-elements set
g /\ e1 is finite Element of bool the carrier of cP
j is non empty finite ( subrelstr e1) Element of bool the carrier of (subrelstr e1)
card j is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
((subrelstr e1)) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
i is finite Element of p1
i /\ j is finite Element of bool the carrier of (subrelstr e1)
r is Element of j
{r} is non empty trivial finite 1 -element Element of bool j
bool j is non empty finite with_finite-elements set
g . r is set
iP \/ {r} is non empty set
s is non empty finite Element of bool the carrier of cP
subrelstr s is non empty finite strict transitive antisymmetric V147(cP) () () SubRelStr of cP
the carrier of (subrelstr s) is non empty finite set
s /\ (iP \/ {r}) is finite set
{ H1(b1) where b1 is finite Element of p1 : S5[b1] } is set
Sp is set
Sp is non empty finite with_finite-elements with_non-empty_elements a_partition of s
bool the carrier of (subrelstr s) is non empty finite with_finite-elements set
Sp is set
cc is finite Element of p1
cc /\ s is finite Element of bool the carrier of cP
Sp is non empty finite with_finite-elements with_non-empty_elements ( subrelstr s) a_partition of the carrier of (subrelstr s)
card Sp is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
i /\ s is finite Element of bool the carrier of cP
s /\ (iP \/ {r}) is finite Element of bool the carrier of cP
d is set
d is set
(iP \/ {r}) /\ d is set
dd is finite Element of p1
dd /\ s is finite Element of bool the carrier of cP
iP /\ dd is finite Element of bool the carrier of (subrelstr e1)
iP /\ d is Element of bool the carrier of cP
{} /\ s is Relation-like finite Element of bool the carrier of cP
{r} /\ d is finite Element of bool j
(iP /\ d) \/ ({r} /\ d) is set
x is set
g is finite (cP) Element of bool the carrier of cP
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
g /\ iP is finite Element of bool the carrier of cP
g is set
g /\ iP is finite Element of bool the carrier of cP
g is set
{g} is non empty trivial finite 1 -element set
g \ {g} is finite Element of bool the carrier of cP
(g \ {g}) \/ {g} is non empty finite set
card (g \ {g}) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(card (g \ {g})) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g is set
g /\ A is finite Element of bool the carrier of cP
g is set
bool the carrier of g is non empty set
g is finite (g) Element of bool the carrier of g
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
g /\ iP is finite Element of bool the carrier of cP
g is non empty with_non-empty_elements (g) a_partition of the carrier of g
card g is non empty epsilon-transitive epsilon-connected ordinal cardinal set
the carrier of cP \ A is Element of bool the carrier of cP
{( the carrier of cP \ A)} is non empty trivial finite 1 -element Element of bool (bool the carrier of cP)
bool (bool the carrier of cP) is non empty set
g \/ {( the carrier of cP \ A)} is non empty set
e1 is set
g is non empty with_non-empty_elements a_partition of the carrier of cP
bool the carrier of g is non empty set
e1 is non empty with_non-empty_elements (cP) a_partition of the carrier of cP
card e1 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
A \/ A is Element of bool the carrier of cP
f is transitive antisymmetric () RelStr
the carrier of f is set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n is transitive antisymmetric () RelStr
(n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of n is set
cP is with_non-empty_elements (n) a_partition of the carrier of n
card cP is epsilon-transitive epsilon-connected ordinal cardinal set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
cP is transitive antisymmetric () RelStr
(cP) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of cP is set
iP is non empty transitive antisymmetric () RelStr
(iP) is non empty (iP) Element of bool the carrier of iP
the carrier of iP is non empty set
bool the carrier of iP is non empty set
the carrier of cP \ (iP) is Element of bool the carrier of cP
bool the carrier of cP is non empty set
g is Element of bool the carrier of cP
subrelstr g is strict transitive antisymmetric V147(cP) () SubRelStr of cP
the carrier of (subrelstr g) is set
g is transitive antisymmetric () RelStr
the carrier of g is set
bool the carrier of g is non empty set
(g) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g is finite (g) Element of bool the carrier of g
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
g is finite (cP) Element of bool the carrier of cP
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
g /\ g is finite Element of bool the carrier of cP
the InternalRel of cP is Relation-like the carrier of cP -defined the carrier of cP -valued Element of bool [: the carrier of cP, the carrier of cP:]
[: the carrier of cP, the carrier of cP:] is Relation-like set
bool [: the carrier of cP, the carrier of cP:] is non empty set
p1 is Element of the carrier of cP
g /\ (iP) is finite Element of bool the carrier of iP
{p1} is non empty trivial finite 1 -element set
p2 is set
[#] cP is non proper Element of bool the carrier of cP
i is Element of the carrier of cP
p2 is set
[#] cP is non proper Element of bool the carrier of cP
i is Element of the carrier of cP
{i} is non empty trivial finite 1 -element set
g \/ {i} is non empty finite set
r is finite (cP) Element of bool the carrier of cP
card r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(card g) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(n + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(n + 1) + 0 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
e2 is finite (g) Element of bool the carrier of g
g /\ the carrier of cP is finite Element of bool the carrier of cP
(g /\ the carrier of cP) \ (g /\ (iP)) is finite Element of bool the carrier of cP
card e2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
card {p1} is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(card g) - (card {p1}) is ext-real V49() real V51() set
(n + 1) - 1 is ext-real V49() real V51() set
the InternalRel of g is Relation-like the carrier of g -defined the carrier of g -valued Element of bool [: the carrier of g, the carrier of g:]
[: the carrier of g, the carrier of g:] is Relation-like set
bool [: the carrier of g, the carrier of g:] is non empty set
p2 is Element of the carrier of g
[#] cP is non proper Element of bool the carrier of cP
i is Element of the carrier of cP
j is Element of the carrier of cP
{j} is non empty trivial finite 1 -element set
g \/ {j} is non empty finite set
s is finite (cP) Element of bool the carrier of cP
card s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
(n + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
p2 is with_non-empty_elements (g) a_partition of the carrier of g
card p2 is epsilon-transitive epsilon-connected ordinal cardinal set
{(iP)} is non empty trivial finite 1 -element Element of bool (bool the carrier of iP)
bool (bool the carrier of iP) is non empty set
p2 \/ {(iP)} is non empty set
g \/ (iP) is non empty set
r is set
r is with_non-empty_elements (cP) a_partition of the carrier of cP
card r is epsilon-transitive epsilon-connected ordinal cardinal set
i is finite set
f is finite transitive antisymmetric () () RelStr
card f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of f is finite set
card the carrier of f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
bool the carrier of f is non empty finite with_finite-elements set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n * cP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(n * cP) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
cP + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(f) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
iP is finite with_finite-elements with_non-empty_elements (f) a_partition of the carrier of f
card iP is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
P is finite (f) Element of bool the carrier of f
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
canFS iP is Relation-like NAT -defined iP -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like FinSequence of iP
len (canFS iP) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of NAT
dom (canFS iP) is finite Element of bool NAT
Seg (len (canFS iP)) is finite len (canFS iP) -element Element of bool NAT
rng (canFS iP) is finite set
g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g is Relation-like NAT -defined bool the carrier of f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool the carrier of f
dom g is finite Element of bool NAT
g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g . g is set
rng g is finite set
g . g is set
e1 is finite Element of bool the carrier of f
e2 is finite Element of bool the carrier of f
union (rng g) is set
card (union (rng g)) is epsilon-transitive epsilon-connected ordinal cardinal set
Card g is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V75() FinSequence of NAT
Sum (Card g) is ext-real V49() real set
(f) -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of NAT
(f) |-> g is Relation-like NAT -defined NAT -valued Function-like finite (f) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of (f) -tuples_on NAT
g is Relation-like NAT -defined NAT -valued Function-like finite (f) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of (f) -tuples_on NAT
Sum g is ext-real V49() real set
(f) * n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
dom (Card g) is finite Element of bool NAT
len (Card g) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of NAT
(f) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
e1 is Relation-like NAT -defined NAT -valued Function-like finite (f) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of (f) -tuples_on NAT
e2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
Seg (f) is finite (f) -element Element of bool NAT
g . e2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
e1 . e2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g . e2 is set
card (g . e2) is epsilon-transitive epsilon-connected ordinal cardinal set
p1 is finite (f) Element of bool the carrier of f
card p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
Sum e1 is ext-real V49() real set
cP * n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(n * cP) + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
card f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n ^2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n * n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
(n ^2) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
[:f,f:] is Relation-like finite set
bool [:f,f:] is non empty finite with_finite-elements set
iP is Relation-like f -defined f -valued finite Element of bool [:f,f:]
RelStr(# f,iP #) is strict RelStr
dom f is finite Element of bool NAT
len f is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of NAT
Seg (len f) is finite len f -element Element of bool NAT
P is set
the carrier of RelStr(# f,iP #) is set
A is set
[P,A] is non empty set
{P,A} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,A},{P}} is non empty finite with_finite-elements set
the InternalRel of RelStr(# f,iP #) is Relation-like the carrier of RelStr(# f,iP #) -defined the carrier of RelStr(# f,iP #) -valued Element of bool [: the carrier of RelStr(# f,iP #), the carrier of RelStr(# f,iP #):]
[: the carrier of RelStr(# f,iP #), the carrier of RelStr(# f,iP #):] is Relation-like set
bool [: the carrier of RelStr(# f,iP #), the carrier of RelStr(# f,iP #):] is non empty set
[A,P] is non empty set
{A,P} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,P},{A}} is non empty finite with_finite-elements set
g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g is ext-real V49() real set
[g,g] is non empty set
{g,g} is non empty finite set
{g} is non empty trivial finite with_finite-elements 1 -element set
{{g,g},{g}} is non empty finite with_finite-elements set
g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g is ext-real V49() real set
[g,g] is non empty set
{g,g} is non empty finite set
{g} is non empty trivial finite with_finite-elements 1 -element set
{{g,g},{g}} is non empty finite with_finite-elements set
g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
e2 is ext-real V49() real set
[g,e2] is non empty set
{g,e2} is non empty finite set
{g} is non empty trivial finite with_finite-elements 1 -element set
{{g,e2},{g}} is non empty finite with_finite-elements set
e1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
p1 is ext-real V49() real set
[e1,p1] is non empty set
{e1,p1} is non empty finite set
{e1} is non empty trivial finite with_finite-elements 1 -element set
{{e1,p1},{e1}} is non empty finite with_finite-elements set
P is set
the carrier of RelStr(# f,iP #) is set
A is set
g is set
[P,A] is non empty set
{P,A} is non empty finite set
{P} is non empty trivial finite 1 -element set
{{P,A},{P}} is non empty finite with_finite-elements set
the InternalRel of RelStr(# f,iP #) is Relation-like the carrier of RelStr(# f,iP #) -defined the carrier of RelStr(# f,iP #) -valued Element of bool [: the carrier of RelStr(# f,iP #), the carrier of RelStr(# f,iP #):]
[: the carrier of RelStr(# f,iP #), the carrier of RelStr(# f,iP #):] is Relation-like set
bool [: the carrier of RelStr(# f,iP #), the carrier of RelStr(# f,iP #):] is non empty set
[A,g] is non empty set
{A,g} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,g},{A}} is non empty finite with_finite-elements set
[P,g] is non empty set
{P,g} is non empty finite set
{{P,g},{P}} is non empty finite with_finite-elements set
g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g is ext-real V49() real set
[g,g] is non empty set
{g,g} is non empty finite set
{g} is non empty trivial finite with_finite-elements 1 -element set
{{g,g},{g}} is non empty finite with_finite-elements set
g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
g is ext-real V49() real set
[g,g] is non empty set
{g,g} is non empty finite set
{g} is non empty trivial finite with_finite-elements 1 -element set
{{g,g},{g}} is non empty finite with_finite-elements set
e1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
p1 is ext-real V49() real set
[e1,p1] is non empty set
{e1,p1} is non empty finite set
{e1} is non empty trivial finite with_finite-elements 1 -element set
{{e1,p1},{e1}} is non empty finite with_finite-elements set
e2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
p2 is ext-real V49() real set
[e2,p2] is non empty set
{e2,p2} is non empty finite set
{e2} is non empty trivial finite with_finite-elements 1 -element set
{{e2,p2},{e2}} is non empty finite with_finite-elements set
P is finite transitive antisymmetric () () RelStr
card P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
the carrier of P is finite set
card the carrier of P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
bool the carrier of P is non empty finite with_finite-elements set
A is finite (P) Element of bool the carrier of P
card A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
A is finite (P) Element of bool the carrier of P
card A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
bool f is non empty finite with_finite-elements set
g is Relation-like NAT -defined Function-like finite complex-valued ext-real-valued real-valued Element of bool f
g is Relation-like Function-like set
dom g is set
g is set
g is set
[g,g] is non empty set
{g,g} is non empty finite set
{g} is non empty trivial finite 1 -element set
{{g,g},{g}} is non empty finite with_finite-elements set
g is Relation-like NAT -defined Function-like finite FinSubsequence-like set
g is Relation-like NAT -defined Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
e1 is ext-real set
dom g is finite set
e2 is ext-real set
g . e2 is ext-real V49() real set
g . e1 is ext-real V49() real set
dom g is finite Element of bool NAT
[e1,(g . e1)] is non empty set
{e1,(g . e1)} is non empty finite set
{e1} is non empty trivial finite 1 -element set
{{e1,(g . e1)},{e1}} is non empty finite with_finite-elements set
[e2,(g . e2)] is non empty set
{e2,(g . e2)} is non empty finite set
{e2} is non empty trivial finite 1 -element set
{{e2,(g . e2)},{e2}} is non empty finite with_finite-elements set
p1 is Element of the carrier of P
p2 is Element of the carrier of P
[p1,p2] is non empty set
{p1,p2} is non empty finite set
{p1} is non empty trivial finite 1 -element set
{{p1,p2},{p1}} is non empty finite with_finite-elements set
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
r is ext-real V49() real set
[i,r] is non empty set
{i,r} is non empty finite set
{i} is non empty trivial finite with_finite-elements 1 -element set
{{i,r},{i}} is non empty finite with_finite-elements set
j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
s is ext-real V49() real set
[j,s] is non empty set
{j,s} is non empty finite set
{j} is non empty trivial finite with_finite-elements 1 -element set
{{j,s},{j}} is non empty finite with_finite-elements set
[p2,p1] is non empty set
{p2,p1} is non empty finite set
{p2} is non empty trivial finite 1 -element set
{{p2,p1},{p2}} is non empty finite with_finite-elements set
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
r is ext-real V49() real set
[i,r] is non empty set
{i,r} is non empty finite set
{i} is non empty trivial finite with_finite-elements 1 -element set
{{i,r},{i}} is non empty finite with_finite-elements set
j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
s is ext-real V49() real set
[j,s] is non empty set
{j,s} is non empty finite set
{j} is non empty trivial finite with_finite-elements 1 -element set
{{j,s},{j}} is non empty finite with_finite-elements set
bool the carrier of P is non empty finite with_finite-elements set
A is finite (P) Element of bool the carrier of P
card A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
A is finite (P) Element of bool the carrier of P
card A is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
bool f is non empty finite with_finite-elements set
g is Relation-like NAT -defined Function-like finite complex-valued ext-real-valued real-valued Element of bool f
g is Relation-like Function-like set
dom g is set
g is set
g is set
[g,g] is non empty set
{g,g} is non empty finite set
{g} is non empty trivial finite 1 -element set
{{g,g},{g}} is non empty finite with_finite-elements set
g is Relation-like NAT -defined Function-like finite FinSubsequence-like set
g is Relation-like NAT -defined Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
card g is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() Element of omega
e1 is ext-real set
dom g is finite set
e2 is ext-real set
g . e1 is ext-real V49() real set
g . e2 is ext-real V49() real set
dom g is finite Element of bool NAT
[e1,(g . e1)] is non empty set
{e1,(g . e1)} is non empty finite set
{e1} is non empty trivial finite 1 -element set
{{e1,(g . e1)},{e1}} is non empty finite with_finite-elements set
[e2,(g . e2)] is non empty set
{e2,(g . e2)} is non empty finite set
{e2} is non empty trivial finite 1 -element set
{{e2,(g . e2)},{e2}} is non empty finite with_finite-elements set
p1 is Element of the carrier of P
p2 is Element of the carrier of P
f . e1 is ext-real V49() real set
f . e2 is ext-real V49() real set
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
r is ext-real V49() real set
[i,r] is non empty set
{i,r} is non empty finite set
{i} is non empty trivial finite with_finite-elements 1 -element set
{{i,r},{i}} is non empty finite with_finite-elements set
j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V49() real V51() set
s is ext-real V49() real set
[j,s] is non empty set
{j,s} is non empty finite set
{j} is non empty trivial finite with_finite-elements 1 -element set
{{j,s},{j}} is non empty finite with_finite-elements set
[p1,p2] is non empty set
{p1,p2} is non empty finite set
{p1} is non empty trivial finite 1 -element set
{{p1,p2},{p1}} is non empty finite with_finite-elements set
bool the carrier of P is non empty finite with_finite-elements set