:: WELLFND1 semantic presentation

REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
NAT is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
bool NAT is non empty non finite set
COMPLEX is set
RAT is set
INT is set
bool NAT is non empty non finite set
{} is empty trivial Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite cardinal {} -element set
the empty trivial Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite cardinal {} -element set is empty trivial Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite cardinal {} -element set
1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of NAT
{{},1} is non empty set
R is functional set
union R is set
c is set
r is set
[c,r] is non empty set
{c,r} is non empty set
{c} is non empty trivial 1 -element set
{{c,r},{c}} is non empty set
Y is set
[c,Y] is non empty set
{c,Y} is non empty set
{{c,Y},{c}} is non empty set
f is set
f is set
n is Relation-like Function-like set
n is Relation-like Function-like set
x is Relation-like Function-like set
c is set
r is set
F₁() is set
F₂() is set
PFuncs (F₁(),F₂()) is non empty functional M14(F₁(),F₂())
bool (PFuncs (F₁(),F₂())) is non empty set
[:F₁(),F₂():] is set
bool [:F₁(),F₂():] is non empty set
R is functional Element of bool (PFuncs (F₁(),F₂()))
c is Relation-like F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
R is set
nextcard R is epsilon-transitive epsilon-connected ordinal cardinal set
R is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal regular set
cf R is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal set
c is set
card c is epsilon-transitive epsilon-connected ordinal cardinal set
sup c is epsilon-transitive epsilon-connected ordinal set
R is RelStr
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is set
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
c is set
the InternalRel of R -Seg c is set
Coim ( the InternalRel of R,c) is set
{c} is non empty trivial 1 -element set
the InternalRel of R " {c} is set
(Coim ( the InternalRel of R,c)) \ {c} is Element of bool (Coim ( the InternalRel of R,c))
bool (Coim ( the InternalRel of R,c)) is non empty set
field the InternalRel of R is set
dom the InternalRel of R is set
rng the InternalRel of R is set
(dom the InternalRel of R) \/ (rng the InternalRel of R) is set
the carrier of R \/ the carrier of R is set
R is RelStr
the carrier of R is set
bool the carrier of R is non empty set
c is Element of bool the carrier of R
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
r is set
Y is set
[Y,r] is non empty set
{Y,r} is non empty set
{Y} is non empty trivial 1 -element set
{{Y,r},{Y}} is non empty set
f is Element of the carrier of R
f is Element of the carrier of R
r is Element of the carrier of R
Y is Element of the carrier of R
[Y,r] is non empty set
{Y,r} is non empty set
{Y} is non empty trivial 1 -element set
{{Y,r},{Y}} is non empty set
R is RelStr
the carrier of R is set
bool the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
c is Element of bool the carrier of R
r is set
the InternalRel of R -Seg r is set
Coim ( the InternalRel of R,r) is set
{r} is non empty trivial 1 -element set
the InternalRel of R " {r} is set
(Coim ( the InternalRel of R,r)) \ {r} is Element of bool (Coim ( the InternalRel of R,r))
bool (Coim ( the InternalRel of R,r)) is non empty set
Y is set
[Y,r] is non empty set
{Y,r} is non empty set
{Y} is non empty trivial 1 -element set
{{Y,r},{Y}} is non empty set
R is RelStr
the carrier of R is set
bool the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
c is lower Element of bool the carrier of R
r is Element of bool the carrier of R
Y is set
{Y} is non empty trivial 1 -element set
c \/ {Y} is non empty set
the InternalRel of R -Seg Y is set
Coim ( the InternalRel of R,Y) is set
the InternalRel of R " {Y} is set
(Coim ( the InternalRel of R,Y)) \ {Y} is Element of bool (Coim ( the InternalRel of R,Y))
bool (Coim ( the InternalRel of R,Y)) is non empty set
f is set
n is set
[n,f] is non empty set
{n,f} is non empty set
{n} is non empty trivial 1 -element set
{{n,f},{n}} is non empty set
{{}} is non empty trivial 1 -element set
[:{{}},{{}}:] is non empty set
bool [:{{}},{{}}:] is non empty set
R is Relation-like {{}} -defined {{}} -valued Element of bool [:{{}},{{}}:]
RelStr(# {{}},R #) is strict RelStr
c is strict RelStr
r is set
the carrier of c is set
the InternalRel of c is Relation-like the carrier of c -defined the carrier of c -valued Element of bool [: the carrier of c, the carrier of c:]
[: the carrier of c, the carrier of c:] is set
bool [: the carrier of c, the carrier of c:] is non empty set
Y is empty trivial Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite cardinal {} -element set
the InternalRel of c -Seg Y is set
Coim ( the InternalRel of c,Y) is set
{Y} is non empty trivial 1 -element set
the InternalRel of c " {Y} is set
(Coim ( the InternalRel of c,Y)) \ {Y} is Element of bool (Coim ( the InternalRel of c,Y))
bool (Coim ( the InternalRel of c,Y)) is non empty set
( the InternalRel of c -Seg Y) /\ r is set
f is set
R is RelStr
the carrier of R is set
bool the carrier of R is non empty set
R is RelStr
the carrier of R is set
bool the carrier of R is non empty set
c is Element of bool the carrier of R
r is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
R is RelStr
the carrier of R is set
bool the carrier of R is non empty set
{ b₁ where b₁ is Element of bool the carrier of R : ( b₁ is (R) & b₁ is lower ) } is set
union { b₁ where b₁ is Element of bool the carrier of R : ( b₁ is (R) & b₁ is lower ) } is set
bool the carrier of R is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
r is set
Y is Element of bool the carrier of R
r is Element of bool (bool the carrier of R)
union r is Element of bool the carrier of R
c is Element of bool the carrier of R
r is Element of bool the carrier of R
R is RelStr
(R) is Element of bool the carrier of R
the carrier of R is set
bool the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
{ b₁ where b₁ is Element of bool the carrier of R : ( b₁ is (R) & b₁ is lower ) } is set
union { b₁ where b₁ is Element of bool the carrier of R : ( b₁ is (R) & b₁ is lower ) } is set
f is set
f is set
[f,f] is non empty set
{f,f} is non empty set
{f} is non empty trivial 1 -element set
{{f,f},{f}} is non empty set
n is set
n is Element of bool the carrier of R
f is set
f is set
n is set
n is Element of bool the carrier of R
f /\ n is Element of bool the carrier of R
x0 is set
the InternalRel of R -Seg x0 is set
Coim ( the InternalRel of R,x0) is set
{x0} is non empty trivial 1 -element set
the InternalRel of R " {x0} is set
(Coim ( the InternalRel of R,x0)) \ {x0} is Element of bool (Coim ( the InternalRel of R,x0))
bool (Coim ( the InternalRel of R,x0)) is non empty set
( the InternalRel of R -Seg x0) /\ f is set
( the InternalRel of R -Seg x0) /\ n is Element of bool the carrier of R
(( the InternalRel of R -Seg x0) /\ n) /\ f is Element of bool the carrier of R
( the InternalRel of R -Seg x0) /\ (f /\ n) is Element of bool the carrier of R
R is non empty RelStr
the carrier of R is non empty set
bool the carrier of R is non empty set
c is Element of the carrier of R
{c} is non empty trivial 1 -element Element of bool the carrier of R
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
Y is Element of bool the carrier of R
f is set
the InternalRel of R -Seg c is set
Coim ( the InternalRel of R,c) is set
{c} is non empty trivial 1 -element set
the InternalRel of R " {c} is set
(Coim ( the InternalRel of R,c)) \ {c} is Element of bool (Coim ( the InternalRel of R,c))
bool (Coim ( the InternalRel of R,c)) is non empty set
( the InternalRel of R -Seg c) /\ f is set
f is set
R is RelStr
the carrier of R is set
bool the carrier of R is non empty set
c is (R) Element of bool the carrier of R
r is (R) Element of bool the carrier of R
c \/ r is Element of bool the carrier of R
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
f is Element of bool the carrier of R
f is set
c /\ f is Element of bool the carrier of R
n is set
the InternalRel of R -Seg n is set
Coim ( the InternalRel of R,n) is set
{n} is non empty trivial 1 -element set
the InternalRel of R " {n} is set
(Coim ( the InternalRel of R,n)) \ {n} is Element of bool (Coim ( the InternalRel of R,n))
bool (Coim ( the InternalRel of R,n)) is non empty set
( the InternalRel of R -Seg n) /\ f is set
x is set
[x,n] is non empty set
{x,n} is non empty set
{x} is non empty trivial 1 -element set
{{x,n},{x}} is non empty set
R is RelStr
(R) is lower (R) Element of bool the carrier of R
the carrier of R is set
bool the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
{ b₁ where b₁ is Element of bool the carrier of R : ( b₁ is (R) & b₁ is lower ) } is set
union { b₁ where b₁ is Element of bool the carrier of R : ( b₁ is (R) & b₁ is lower ) } is set
f is Element of bool the carrier of R
n is set
n is set
[n,n] is non empty set
{n,n} is non empty set
{n} is non empty trivial 1 -element set
{{n,n},{n}} is non empty set
n is set
n is set
x is set
x0 is Element of bool the carrier of R
n /\ x0 is Element of bool the carrier of R
gr is set
the InternalRel of R -Seg gr is set
Coim ( the InternalRel of R,gr) is set
{gr} is non empty trivial 1 -element set
the InternalRel of R " {gr} is set
(Coim ( the InternalRel of R,gr)) \ {gr} is Element of bool (Coim ( the InternalRel of R,gr))
bool (Coim ( the InternalRel of R,gr)) is non empty set
( the InternalRel of R -Seg gr) /\ n is set
( the InternalRel of R -Seg gr) /\ x0 is Element of bool the carrier of R
(( the InternalRel of R -Seg gr) /\ x0) /\ n is Element of bool the carrier of R
( the InternalRel of R -Seg gr) /\ (n /\ x0) is Element of bool the carrier of R
R is non empty RelStr
the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
(R) is lower (R) Element of bool the carrier of R
bool the carrier of R is non empty set
c is Element of the carrier of R
the InternalRel of R -Seg c is set
Coim ( the InternalRel of R,c) is set
{c} is non empty trivial 1 -element set
the InternalRel of R " {c} is set
(Coim ( the InternalRel of R,c)) \ {c} is Element of bool (Coim ( the InternalRel of R,c))
bool (Coim ( the InternalRel of R,c)) is non empty set
{ b₁ where b₁ is Element of bool the carrier of R : ( b₁ is (R) & b₁ is lower ) } is set
{c} is non empty trivial 1 -element Element of bool the carrier of R
(R) \/ {c} is non empty Element of bool the carrier of R
union { b₁ where b₁ is Element of bool the carrier of R : ( b₁ is (R) & b₁ is lower ) } is set
f is Element of bool the carrier of R
F₁() is non empty RelStr
the carrier of F₁() is non empty set
F₂() is Element of 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 set
bool [: the carrier of F₁(), the carrier of F₁():] is non empty set
{ b₁ where b₁ is Element of the carrier of F₁() : P₁[b₁] } is set
bool the carrier of F₁() is non empty set
Y is non empty Element of bool the carrier of F₁()
f is set
the InternalRel of F₁() -Seg f is set
Coim ( the InternalRel of F₁(),f) is set
{f} is non empty trivial 1 -element set
the InternalRel of F₁() " {f} is set
(Coim ( the InternalRel of F₁(),f)) \ {f} is Element of bool (Coim ( the InternalRel of F₁(),f))
bool (Coim ( the InternalRel of F₁(),f)) is non empty set
f is Element of the carrier of F₁()
n is Element of the carrier of F₁()
n is Element of the carrier of F₁()
[n,f] is non empty Element of [: the carrier of F₁(), the carrier of F₁():]
{n,f} is non empty set
{n} is non empty trivial 1 -element set
{{n,f},{n}} is non empty set
the InternalRel of F₁() -Seg f is set
Coim ( the InternalRel of F₁(),f) is set
{f} is non empty trivial 1 -element set
the InternalRel of F₁() " {f} is set
(Coim ( the InternalRel of F₁(),f)) \ {f} is Element of bool (Coim ( the InternalRel of F₁(),f))
bool (Coim ( the InternalRel of F₁(),f)) is non empty set
R is non empty RelStr
the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
Y is set
f is set
f is Element of the carrier of R
n is Element of the carrier of R
the InternalRel of R -Seg n is set
Coim ( the InternalRel of R,n) is set
{n} is non empty trivial 1 -element set
the InternalRel of R " {n} is set
(Coim ( the InternalRel of R,n)) \ {n} is Element of bool (Coim ( the InternalRel of R,n))
bool (Coim ( the InternalRel of R,n)) is non empty set
n is set
[n,n] is non empty set
{n,n} is non empty set
{n} is non empty trivial 1 -element set
{{n,n},{n}} is non empty set
x is Element of the carrier of R
Y is set
f is Element of the carrier of R
the InternalRel of R -Seg f is set
Coim ( the InternalRel of R,f) is set
{f} is non empty trivial 1 -element set
the InternalRel of R " {f} is set
(Coim ( the InternalRel of R,f)) \ {f} is Element of bool (Coim ( the InternalRel of R,f))
bool (Coim ( the InternalRel of R,f)) is non empty set
the carrier of R \ Y is Element of bool the carrier of R
bool the carrier of R is non empty set
f is set
F₁() is non empty RelStr
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 set
bool [: the carrier of F₁(), the carrier of F₁():] is non empty set
{ b₁ where b₁ is Element of the carrier of F₁() : P₁[b₁] } is set
Y is Element of the carrier of F₁()
the InternalRel of F₁() -Seg Y is set
Coim ( the InternalRel of F₁(),Y) is set
{Y} is non empty trivial 1 -element set
the InternalRel of F₁() " {Y} is set
(Coim ( the InternalRel of F₁(),Y)) \ {Y} is Element of bool (Coim ( the InternalRel of F₁(),Y))
bool (Coim ( the InternalRel of F₁(),Y)) is non empty set
f is Element of the carrier of F₁()
f is Element of the carrier of F₁()
[f,f] is non empty Element of [: the carrier of F₁(), the carrier of F₁():]
{f,f} is non empty set
{f} is non empty trivial 1 -element set
{{f,f},{f}} is non empty set
the InternalRel of F₁() -Seg f is set
Coim ( the InternalRel of F₁(),f) is set
{f} is non empty trivial 1 -element set
the InternalRel of F₁() " {f} is set
(Coim ( the InternalRel of F₁(),f)) \ {f} is Element of bool (Coim ( the InternalRel of F₁(),f))
bool (Coim ( the InternalRel of F₁(),f)) is non empty set
n is Element of the carrier of F₁()
Y is Element of the carrier of F₁()
f is Element of the carrier of F₁()
R is non empty RelStr
the carrier of R is non empty set
c is non empty set
PFuncs ( the carrier of R,c) is non empty functional M14( the carrier of R,c)
[: the carrier of R,(PFuncs ( the carrier of R,c)):] is non empty set
[:[: the carrier of R,(PFuncs ( the carrier of R,c)):],c:] is non empty set
bool [:[: the carrier of R,(PFuncs ( the carrier of R,c)):],c:] is non empty set
R is non empty RelStr
the carrier of R is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
card the carrier of R is non empty epsilon-transitive epsilon-connected ordinal cardinal set
NAT +` (card the carrier of R) is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal set
Y is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal set
nextcard Y is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal set
PFuncs ( the carrier of R,(nextcard Y)) is non empty functional M14( the carrier of R, nextcard Y)
f is Element of the carrier of R
n is Relation-like the carrier of R -defined nextcard Y -valued Function-like Element of PFuncs ( the carrier of R,(nextcard Y))
rng n is Element of bool (nextcard Y)
bool (nextcard Y) is non empty non finite set
sup (rng n) is epsilon-transitive epsilon-connected ordinal set
dom n is Element of bool the carrier of R
bool the carrier of R is non empty set
card (dom n) is epsilon-transitive epsilon-connected ordinal cardinal set
card (rng n) is epsilon-transitive epsilon-connected ordinal cardinal set
[: the carrier of R,(PFuncs ( the carrier of R,(nextcard Y))):] is non empty set
[:[: the carrier of R,(PFuncs ( the carrier of R,(nextcard Y))):],(nextcard Y):] is non empty non finite set
bool [:[: the carrier of R,(PFuncs ( the carrier of R,(nextcard Y))):],(nextcard Y):] is non empty non finite set
f is Relation-like [: the carrier of R,(PFuncs ( the carrier of R,(nextcard Y))):] -defined nextcard Y -valued Function-like V23([: the carrier of R,(PFuncs ( the carrier of R,(nextcard Y))):], nextcard Y) Element of bool [:[: the carrier of R,(PFuncs ( the carrier of R,(nextcard Y))):],(nextcard Y):]
n is non empty set
PFuncs ( the carrier of R,n) is non empty functional M14( the carrier of R,n)
[: the carrier of R,(PFuncs ( the carrier of R,n)):] is non empty set
[:[: the carrier of R,(PFuncs ( the carrier of R,n)):],n:] is non empty set
bool [:[: the carrier of R,(PFuncs ( the carrier of R,n)):],n:] is non empty set
[: the carrier of R,n:] is non empty set
bool [: the carrier of R,n:] is non empty set
n is Relation-like [: the carrier of R,(PFuncs ( the carrier of R,n)):] -defined n -valued Function-like V23([: the carrier of R,(PFuncs ( the carrier of R,n)):],n) Element of bool [:[: the carrier of R,(PFuncs ( the carrier of R,n)):],n:]
bool (PFuncs ( the carrier of R,n)) is non empty set
x is functional Element of bool (PFuncs ( the carrier of R,n))
x0 is Relation-like Function-like set
fr is Relation-like Function-like set
gr is Relation-like the carrier of R -defined n -valued Function-like Element of bool [: the carrier of R,n:]
dom gr is Element of bool the carrier of R
bool the carrier of R is non empty set
x1 is Relation-like the carrier of R -defined n -valued Function-like Element of bool [: the carrier of R,n:]
dom x1 is Element of bool the carrier of R
(dom gr) /\ (dom x1) is Element of bool the carrier of R
x1 is set
gr . x1 is set
x1 . x1 is set
F2 is Element of the carrier of R
gr . F2 is set
x1 . F2 is set
F1 is Element of the carrier of R
gr . F1 is set
x1 . F1 is set
the InternalRel of R -Seg F1 is set
Coim ( the InternalRel of R,F1) is set
{F1} is non empty trivial 1 -element set
the InternalRel of R " {F1} is set
(Coim ( the InternalRel of R,F1)) \ {F1} is Element of bool (Coim ( the InternalRel of R,F1))
bool (Coim ( the InternalRel of R,F1)) is non empty set
gr | ( the InternalRel of R -Seg F1) is Relation-like the carrier of R -defined n -valued Function-like Element of bool [: the carrier of R,n:]
x1 | ( the InternalRel of R -Seg F1) is Relation-like the carrier of R -defined n -valued Function-like Element of bool [: the carrier of R,n:]
dom (gr | ( the InternalRel of R -Seg F1)) is Element of bool the carrier of R
dom (x1 | ( the InternalRel of R -Seg F1)) is Element of bool the carrier of R
F1r is set
(gr | ( the InternalRel of R -Seg F1)) . F1r is set
(x1 | ( the InternalRel of R -Seg F1)) . F1r is set
[F1r,F1] is non empty set
{F1r,F1} is non empty set
{F1r} is non empty trivial 1 -element set
{{F1r,F1},{F1r}} is non empty set
z is Element of the carrier of R
(gr | ( the InternalRel of R -Seg F1)) . z is set
gr . z is set
(x1 | ( the InternalRel of R -Seg F1)) . z is set
x1 . z is set
[F1,(x1 | ( the InternalRel of R -Seg F1))] is non empty Element of [: the carrier of R,(bool [: the carrier of R,n:]):]
[: the carrier of R,(bool [: the carrier of R,n:]):] is non empty set
{F1,(x1 | ( the InternalRel of R -Seg F1))} is non empty set
{{F1,(x1 | ( the InternalRel of R -Seg F1))},{F1}} is non empty set
n . [F1,(x1 | ( the InternalRel of R -Seg F1))] is set
union x is set
fr is set
x0 is Relation-like Function-like set
dom x0 is set
x0 . fr is set
[fr,(x0 . fr)] is non empty set
{fr,(x0 . fr)} is non empty set
{fr} is non empty trivial 1 -element set
{{fr,(x0 . fr)},{fr}} is non empty set
gr is set
x1 is Relation-like the carrier of R -defined n -valued Function-like Element of bool [: the carrier of R,n:]
dom x1 is Element of bool the carrier of R
x1 . fr is set
the InternalRel of R -Seg fr is set
Coim ( the InternalRel of R,fr) is set
the InternalRel of R " {fr} is set
(Coim ( the InternalRel of R,fr)) \ {fr} is Element of bool (Coim ( the InternalRel of R,fr))
bool (Coim ( the InternalRel of R,fr)) is non empty set
x1 | ( the InternalRel of R -Seg fr) is Relation-like the carrier of R -defined n -valued Function-like Element of bool [: the carrier of R,n:]
[fr,(x1 | ( the InternalRel of R -Seg fr))] is non empty set
{fr,(x1 | ( the InternalRel of R -Seg fr))} is non empty set
{{fr,(x1 | ( the InternalRel of R -Seg fr))},{fr}} is non empty set
n . [fr,(x1 | ( the InternalRel of R -Seg fr))] is set
x0 | ( the InternalRel of R -Seg fr) is Relation-like Function-like set
[fr,(x0 | ( the InternalRel of R -Seg fr))] is non empty set
{fr,(x0 | ( the InternalRel of R -Seg fr))} is non empty set
{{fr,(x0 | ( the InternalRel of R -Seg fr))},{fr}} is non empty set
n . [fr,(x0 | ( the InternalRel of R -Seg fr))] is set
fr is set
x0 . fr is set
[fr,(x0 . fr)] is non empty set
{fr,(x0 . fr)} is non empty set
{fr} is non empty trivial 1 -element set
{{fr,(x0 . fr)},{fr}} is non empty set
gr is set
x1 is Relation-like Function-like set
dom x1 is set
rng x1 is set
rng x0 is set
fr is set
gr is set
x0 . gr is set
[gr,fr] is non empty set
{gr,fr} is non empty set
{gr} is non empty trivial 1 -element set
{{gr,fr},{gr}} is non empty set
x1 is set
x1 is Relation-like Function-like set
dom x1 is set
rng x1 is set
fr is set
gr is set
[gr,fr] is non empty set
{gr,fr} is non empty set
{gr} is non empty trivial 1 -element set
{{gr,fr},{gr}} is non empty set
x0 . fr is set
[fr,(x0 . fr)] is non empty set
{fr,(x0 . fr)} is non empty set
{fr} is non empty trivial 1 -element set
{{fr,(x0 . fr)},{fr}} is non empty set
x1 is set
x1 is Relation-like the carrier of R -defined n -valued Function-like Element of bool [: the carrier of R,n:]
dom x1 is Element of bool the carrier of R
fr is set
gr is Element of the carrier of R
x1 is Element of the carrier of R
the InternalRel of R -Seg x1 is set
Coim ( the InternalRel of R,x1) is set
{x1} is non empty trivial 1 -element set
the InternalRel of R " {x1} is set
(Coim ( the InternalRel of R,x1)) \ {x1} is Element of bool (Coim ( the InternalRel of R,x1))
bool (Coim ( the InternalRel of R,x1)) is non empty set
x0 | ( the InternalRel of R -Seg x1) is Relation-like Function-like set
[x1,(x0 | ( the InternalRel of R -Seg x1))] is non empty set
{x1,(x0 | ( the InternalRel of R -Seg x1))} is non empty set
{{x1,(x0 | ( the InternalRel of R -Seg x1))},{x1}} is non empty set
n . [x1,(x0 | ( the InternalRel of R -Seg x1))] is set
x1 .--> (n . [x1,(x0 | ( the InternalRel of R -Seg x1))]) is Relation-like the carrier of R -defined {x1} -defined Function-like one-to-one set
{x1} --> (n . [x1,(x0 | ( the InternalRel of R -Seg x1))]) is non empty Relation-like {x1} -defined {(n . [x1,(x0 | ( the InternalRel of R -Seg x1))])} -valued Function-like constant total V23({x1},{(n . [x1,(x0 | ( the InternalRel of R -Seg x1))])}) Element of bool [:{x1},{(n . [x1,(x0 | ( the InternalRel of R -Seg x1))])}:]
{(n . [x1,(x0 | ( the InternalRel of R -Seg x1))])} is non empty trivial 1 -element set
[:{x1},{(n . [x1,(x0 | ( the InternalRel of R -Seg x1))])}:] is non empty set
bool [:{x1},{(n . [x1,(x0 | ( the InternalRel of R -Seg x1))])}:] is non empty set
x0 +* (x1 .--> (n . [x1,(x0 | ( the InternalRel of R -Seg x1))])) is Relation-like Function-like set
dom (x1 .--> (n . [x1,(x0 | ( the InternalRel of R -Seg x1))])) is trivial Element of bool {x1}
bool {x1} is non empty set
{x1} is non empty trivial 1 -element Element of bool the carrier of R
rng (x0 +* (x1 .--> (n . [x1,(x0 | ( the InternalRel of R -Seg x1))]))) is set
F1 is set
rng (x1 .--> (n . [x1,(x0 | ( the InternalRel of R -Seg x1))])) is set
(rng x0) \/ (rng (x1 .--> (n . [x1,(x0 | ( the InternalRel of R -Seg x1))]))) is set
n . (x1,(x0 | ( the InternalRel of R -Seg x1))) is set
dom (x0 +* (x1 .--> (n . [x1,(x0 | ( the InternalRel of R -Seg x1))]))) is set
(dom x0) \/ (dom (x1 .--> (n . [x1,(x0 | ( the InternalRel of R -Seg x1))]))) is set
F1 is set
(x0 +* (x1 .--> (n . [x1,(x0 | ( the InternalRel of R -Seg x1))]))) . x1 is set
[x1,((x0 +* (x1 .--> (n . [x1,(x0 | ( the InternalRel of R -Seg x1))]))) . x1)] is non empty set
{x1,((x0 +* (x1 .--> (n . [x1,(x0 | ( the InternalRel of R -Seg x1))]))) . x1)} is non empty set
{{x1,((x0 +* (x1 .--> (n . [x1,(x0 | ( the InternalRel of R -Seg x1))]))) . x1)},{x1}} is non empty set
x is set
F1 is Relation-like the carrier of R -defined n -valued Function-like Element of bool [: the carrier of R,n:]
dom F1 is Element of bool the carrier of R
the InternalRel of R -Seg x is set
Coim ( the InternalRel of R,x) is set
{x} is non empty trivial 1 -element set
the InternalRel of R " {x} is set
(Coim ( the InternalRel of R,x)) \ {x} is Element of bool (Coim ( the InternalRel of R,x))
bool (Coim ( the InternalRel of R,x)) is non empty set
x is set
[x1,x] is non empty set
{x1,x} is non empty set
{{x1,x},{x1}} is non empty set
F1 . x is set
x0 . x is set
x0 | ( the InternalRel of R -Seg x) is Relation-like Function-like set
[x,(x0 | ( the InternalRel of R -Seg x))] is non empty set
{x,(x0 | ( the InternalRel of R -Seg x))} is non empty set
{{x,(x0 | ( the InternalRel of R -Seg x))},{x}} is non empty set
n . [x,(x0 | ( the InternalRel of R -Seg x))] is set
F1 | ( the InternalRel of R -Seg x) is Relation-like the carrier of R -defined n -valued Function-like Element of bool [: the carrier of R,n:]
[x,(F1 | ( the InternalRel of R -Seg x))] is non empty set
{x,(F1 | ( the InternalRel of R -Seg x))} is non empty set
{{x,(F1 | ( the InternalRel of R -Seg x))},{x}} is non empty set
n . [x,(F1 | ( the InternalRel of R -Seg x))] is set
x is set
F1 . x is set
(x1 .--> (n . [x1,(x0 | ( the InternalRel of R -Seg x1))])) . x1 is set
the InternalRel of R -Seg x is set
Coim ( the InternalRel of R,x) is set
{x} is non empty trivial 1 -element set
the InternalRel of R " {x} is set
(Coim ( the InternalRel of R,x)) \ {x} is Element of bool (Coim ( the InternalRel of R,x))
bool (Coim ( the InternalRel of R,x)) is non empty set
F1 | ( the InternalRel of R -Seg x) is Relation-like the carrier of R -defined n -valued Function-like Element of bool [: the carrier of R,n:]
[x,(F1 | ( the InternalRel of R -Seg x))] is non empty set
{x,(F1 | ( the InternalRel of R -Seg x))} is non empty set
{{x,(F1 | ( the InternalRel of R -Seg x))},{x}} is non empty set
n . [x,(F1 | ( the InternalRel of R -Seg x))] is set
x is set
x is set
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial 1 -element set
{{x,x},{x}} is non empty set
F1r is Element of the carrier of R
F1 . x1 is set
[x1,(F1 . x1)] is non empty set
{x1,(F1 . x1)} is non empty set
{{x1,(F1 . x1)},{x1}} is non empty set
fr is Relation-like the carrier of R -defined n -valued Function-like V23( the carrier of R,n) Element of bool [: the carrier of R,n:]
gr is Element of the carrier of R
fr . gr is set
the InternalRel of R -Seg gr is set
Coim ( the InternalRel of R,gr) is set
{gr} is non empty trivial 1 -element set
the InternalRel of R " {gr} is set
(Coim ( the InternalRel of R,gr)) \ {gr} is Element of bool (Coim ( the InternalRel of R,gr))
bool (Coim ( the InternalRel of R,gr)) is non empty set
fr | ( the InternalRel of R -Seg gr) is Relation-like Function-like set
n . (gr,(fr | ( the InternalRel of R -Seg gr))) is set
[gr,(fr | ( the InternalRel of R -Seg gr))] is non empty set
{gr,(fr | ( the InternalRel of R -Seg gr))} is non empty set
{{gr,(fr | ( the InternalRel of R -Seg gr))},{gr}} is non empty set
n . [gr,(fr | ( the InternalRel of R -Seg gr))] is set
[: the carrier of R,(nextcard Y):] is non empty non finite set
bool [: the carrier of R,(nextcard Y):] is non empty non finite set
n is Relation-like the carrier of R -defined nextcard Y -valued Function-like V23( the carrier of R, nextcard Y) Element of bool [: the carrier of R,(nextcard Y):]
n is set
n .: n is Element of bool (nextcard Y)
bool (nextcard Y) is non empty non finite set
inf (n .: n) is epsilon-transitive epsilon-connected ordinal set
x0 is set
dom n is Element of bool the carrier of R
bool the carrier of R is non empty set
n . x0 is set
fr is set
n . fr is set
the InternalRel of R -Seg fr is set
Coim ( the InternalRel of R,fr) is set
{fr} is non empty trivial 1 -element set
the InternalRel of R " {fr} is set
(Coim ( the InternalRel of R,fr)) \ {fr} is Element of bool (Coim ( the InternalRel of R,fr))
bool (Coim ( the InternalRel of R,fr)) is non empty set
( the InternalRel of R -Seg fr) /\ n is set
gr is set
x1 is Element of the carrier of R
the InternalRel of R -Seg x1 is set
Coim ( the InternalRel of R,x1) is set
{x1} is non empty trivial 1 -element set
the InternalRel of R " {x1} is set
(Coim ( the InternalRel of R,x1)) \ {x1} is Element of bool (Coim ( the InternalRel of R,x1))
bool (Coim ( the InternalRel of R,x1)) is non empty set
n | ( the InternalRel of R -Seg x1) is Relation-like the carrier of R -defined nextcard Y -valued Function-like Element of bool [: the carrier of R,(nextcard Y):]
n . x1 is epsilon-transitive epsilon-connected ordinal Element of nextcard Y
x1 is Relation-like the carrier of R -defined nextcard Y -valued Function-like Element of PFuncs ( the carrier of R,(nextcard Y))
f . (x1,x1) is epsilon-transitive epsilon-connected ordinal Element of nextcard Y
[x1,x1] is non empty set
{x1,x1} is non empty set
{{x1,x1},{x1}} is non empty set
f . [x1,x1] is set
rng x1 is Element of bool (nextcard Y)
sup (rng x1) is epsilon-transitive epsilon-connected ordinal set
n . gr is set
F2 is epsilon-transitive epsilon-connected ordinal set
R is non empty RelStr
the carrier of R is non empty set
c is non empty non trivial set
PFuncs ( the carrier of R,c) is non empty functional M14( the carrier of R,c)
[: the carrier of R,(PFuncs ( the carrier of R,c)):] is non empty set
[:[: the carrier of R,(PFuncs ( the carrier of R,c)):],c:] is non empty set
bool [:[: the carrier of R,(PFuncs ( the carrier of R,c)):],c:] is non empty set
[: the carrier of R,c:] is non empty set
bool [: the carrier of R,c:] is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
(R) is lower (R) Element of bool the carrier of R
bool the carrier of R is non empty set
n is set
n is set
the carrier of R --> n is non empty Relation-like the carrier of R -defined {n} -valued Function-like constant total V23( the carrier of R,{n}) Element of bool [: the carrier of R,{n}:]
{n} is non empty trivial 1 -element set
[: the carrier of R,{n}:] is non empty set
bool [: the carrier of R,{n}:] is non empty set
(R) --> n is Relation-like (R) -defined {n} -valued Function-like constant total V23((R),{n}) Element of bool [:(R),{n}:]
{n} is non empty trivial 1 -element set
[:(R),{n}:] is set
bool [:(R),{n}:] is non empty set
( the carrier of R --> n) +* ((R) --> n) is Relation-like Function-like set
dom ( the carrier of R --> n) is Element of bool the carrier of R
{n,n} is non empty set
F1 is Relation-like the carrier of R -defined c -valued Function-like Element of PFuncs ( the carrier of R,c)
dom F1 is Element of bool the carrier of R
x1 is Element of {n,n}
F2 is Element of the carrier of R
x is Element of {n,n}
dom F1 is set
x is set
F1 . x is set
F1r is set
F1 . F1r is set
F1 is Relation-like the carrier of R -defined c -valued Function-like Element of PFuncs ( the carrier of R,c)
dom F1 is Element of bool the carrier of R
x1 is Element of {n,n}
F2 is Element of the carrier of R
x is Element of {n,n}
dom F1 is set
x is set
F1 . x is set
F1 is Relation-like the carrier of R -defined c -valued Function-like Element of PFuncs ( the carrier of R,c)
dom F1 is Element of bool the carrier of R
x is set
F1 . x is set
[:[: the carrier of R,(PFuncs ( the carrier of R,c)):],{n,n}:] is non empty set
bool [:[: the carrier of R,(PFuncs ( the carrier of R,c)):],{n,n}:] is non empty set
x1 is Relation-like [: the carrier of R,(PFuncs ( the carrier of R,c)):] -defined {n,n} -valued Function-like V23([: the carrier of R,(PFuncs ( the carrier of R,c)):],{n,n}) Element of bool [:[: the carrier of R,(PFuncs ( the carrier of R,c)):],{n,n}:]
rng x1 is Element of bool {n,n}
bool {n,n} is non empty set
rng ( the carrier of R --> n) is trivial Element of bool {n}
bool {n} is non empty set
rng ((R) --> n) is trivial Element of bool {n}
bool {n} is non empty set
(rng ( the carrier of R --> n)) \/ (rng ((R) --> n)) is set
{n} \/ {n} is non empty set
rng (( the carrier of R --> n) +* ((R) --> n)) is set
dom x1 is Relation-like the carrier of R -defined PFuncs ( the carrier of R,c) -valued Element of bool [: the carrier of R,(PFuncs ( the carrier of R,c)):]
bool [: the carrier of R,(PFuncs ( the carrier of R,c)):] is non empty set
dom ((R) --> n) is Element of bool (R)
bool (R) is non empty set
dom (( the carrier of R --> n) +* ((R) --> n)) is set
(dom ( the carrier of R --> n)) \/ (dom ((R) --> n)) is set
x1 is Relation-like [: the carrier of R,(PFuncs ( the carrier of R,c)):] -defined c -valued Function-like V23([: the carrier of R,(PFuncs ( the carrier of R,c)):],c) Element of bool [:[: the carrier of R,(PFuncs ( the carrier of R,c)):],c:]
F2 is Relation-like the carrier of R -defined c -valued Function-like V23( the carrier of R,c) Element of bool [: the carrier of R,c:]
F1 is Element of the carrier of R
F2 . F1 is set
the InternalRel of R -Seg F1 is set
Coim ( the InternalRel of R,F1) is set
{F1} is non empty trivial 1 -element set
the InternalRel of R " {F1} is set
(Coim ( the InternalRel of R,F1)) \ {F1} is Element of bool (Coim ( the InternalRel of R,F1))
bool (Coim ( the InternalRel of R,F1)) is non empty set
F2 | ( the InternalRel of R -Seg F1) is Relation-like Function-like set
x1 . (F1,(F2 | ( the InternalRel of R -Seg F1))) is set
[F1,(F2 | ( the InternalRel of R -Seg F1))] is non empty set
{F1,(F2 | ( the InternalRel of R -Seg F1))} is non empty set
{{F1,(F2 | ( the InternalRel of R -Seg F1))},{F1}} is non empty set
x1 . [F1,(F2 | ( the InternalRel of R -Seg F1))] is set
F2 | ( the InternalRel of R -Seg F1) is Relation-like the carrier of R -defined c -valued Function-like Element of bool [: the carrier of R,c:]
x is set
x is Relation-like the carrier of R -defined c -valued Function-like Element of PFuncs ( the carrier of R,c)
dom x is Element of bool the carrier of R
x . x is set
F2 . x is set
((R) --> n) . x is set
x1 . (F1,x) is Element of c
[F1,x] is non empty set
{F1,x} is non empty set
{{F1,x},{F1}} is non empty set
x1 . [F1,x] is set
[F1,x] is non empty Element of [: the carrier of R,(PFuncs ( the carrier of R,c)):]
x1 . [F1,x] is Element of c
rng x1 is Element of bool c
bool c is non empty set
((R) --> n) . F1 is set
F2 . F1 is Element of c
x1 . (F1,(F2 | ( the InternalRel of R -Seg F1))) is set
[F1,(F2 | ( the InternalRel of R -Seg F1))] is non empty set
{F1,(F2 | ( the InternalRel of R -Seg F1))} is non empty set
{{F1,(F2 | ( the InternalRel of R -Seg F1))},{F1}} is non empty set
x1 . [F1,(F2 | ( the InternalRel of R -Seg F1))] is set
x is set
x is Relation-like the carrier of R -defined c -valued Function-like Element of PFuncs ( the carrier of R,c)
dom x is Element of bool the carrier of R
x . x is set
F2 . x is set
( the carrier of R --> n) . x is set
F2 . F1 is Element of c
( the carrier of R --> n) . F1 is Element of {n}
x1 . (F1,(F2 | ( the InternalRel of R -Seg F1))) is set
[F1,(F2 | ( the InternalRel of R -Seg F1))] is non empty set
{F1,(F2 | ( the InternalRel of R -Seg F1))} is non empty set
{{F1,(F2 | ( the InternalRel of R -Seg F1))},{F1}} is non empty set
x1 . [F1,(F2 | ( the InternalRel of R -Seg F1))] is set
the carrier of R --> n is non empty Relation-like the carrier of R -defined {n} -valued Function-like constant total V23( the carrier of R,{n}) Element of bool [: the carrier of R,{n}:]
[: the carrier of R,{n}:] is non empty set
bool [: the carrier of R,{n}:] is non empty set
x is set
F1 is Relation-like the carrier of R -defined c -valued Function-like V23( the carrier of R,c) Element of bool [: the carrier of R,c:]
x is Element of the carrier of R
F1 . x is set
the InternalRel of R -Seg x is set
Coim ( the InternalRel of R,x) is set
{x} is non empty trivial 1 -element set
the InternalRel of R " {x} is set
(Coim ( the InternalRel of R,x)) \ {x} is Element of bool (Coim ( the InternalRel of R,x))
bool (Coim ( the InternalRel of R,x)) is non empty set
F1 | ( the InternalRel of R -Seg x) is Relation-like Function-like set
x1 . (x,(F1 | ( the InternalRel of R -Seg x))) is set
[x,(F1 | ( the InternalRel of R -Seg x))] is non empty set
{x,(F1 | ( the InternalRel of R -Seg x))} is non empty set
{{x,(F1 | ( the InternalRel of R -Seg x))},{x}} is non empty set
x1 . [x,(F1 | ( the InternalRel of R -Seg x))] is set
F1 | ( the InternalRel of R -Seg x) is Relation-like the carrier of R -defined c -valued Function-like Element of bool [: the carrier of R,c:]
F1r is Relation-like the carrier of R -defined c -valued Function-like Element of PFuncs ( the carrier of R,c)
[x,F1r] is non empty Element of [: the carrier of R,(PFuncs ( the carrier of R,c)):]
{x,F1r} is non empty set
{{x,F1r},{x}} is non empty set
x1 . [x,F1r] is Element of c
rng x1 is Element of bool c
bool c is non empty set
z is set
dom F1r is Element of bool the carrier of R
F1r . z is set
F1 . z is set
x1 . (x,F1r) is Element of c
[x,F1r] is non empty set
x1 . [x,F1r] is set
F1 . x is Element of c
x1 . (x,(F1 | ( the InternalRel of R -Seg x))) is set
[x,(F1 | ( the InternalRel of R -Seg x))] is non empty set
{x,(F1 | ( the InternalRel of R -Seg x))} is non empty set
{{x,(F1 | ( the InternalRel of R -Seg x))},{x}} is non empty set
x1 . [x,(F1 | ( the InternalRel of R -Seg x))] is set
F1 . x is set
F2 . x is set
( the carrier of R --> n) . x is set
R is non empty () RelStr
the carrier of R is non empty set
c is non empty set
PFuncs ( the carrier of R,c) is non empty functional M14( the carrier of R,c)
[: the carrier of R,(PFuncs ( the carrier of R,c)):] is non empty set
[:[: the carrier of R,(PFuncs ( the carrier of R,c)):],c:] is non empty set
bool [:[: the carrier of R,(PFuncs ( the carrier of R,c)):],c:] is non empty set
[: the carrier of R,c:] is non empty set
bool [: the carrier of R,c:] is non empty set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
f is Relation-like [: the carrier of R,(PFuncs ( the carrier of R,c)):] -defined c -valued Function-like V23([: the carrier of R,(PFuncs ( the carrier of R,c)):],c) Element of bool [:[: the carrier of R,(PFuncs ( the carrier of R,c)):],c:]
f is Relation-like the carrier of R -defined c -valued Function-like V23( the carrier of R,c) Element of bool [: the carrier of R,c:]
n is Relation-like the carrier of R -defined c -valued Function-like V23( the carrier of R,c) Element of bool [: the carrier of R,c:]
dom n is Element of bool the carrier of R
bool the carrier of R is non empty set
n is Element of the carrier of R
f . n is Element of c
n . n is Element of c
x is Element of the carrier of R
f . x is set
n . x is set
x0 is Element of the carrier of R
f . x0 is set
n . x0 is set
dom f is Element of bool the carrier of R
the InternalRel of R -Seg x0 is set
Coim ( the InternalRel of R,x0) is set
{x0} is non empty trivial 1 -element set
the InternalRel of R " {x0} is set
(Coim ( the InternalRel of R,x0)) \ {x0} is Element of bool (Coim ( the InternalRel of R,x0))
bool (Coim ( the InternalRel of R,x0)) is non empty set
f | ( the InternalRel of R -Seg x0) is Relation-like the carrier of R -defined c -valued Function-like Element of bool [: the carrier of R,c:]
n | ( the InternalRel of R -Seg x0) is Relation-like the carrier of R -defined c -valued Function-like Element of bool [: the carrier of R,c:]
dom (f | ( the InternalRel of R -Seg x0)) is Element of bool the carrier of R
dom (n | ( the InternalRel of R -Seg x0)) is Element of bool the carrier of R
x1 is set
(f | ( the InternalRel of R -Seg x0)) . x1 is set
(n | ( the InternalRel of R -Seg x0)) . x1 is set
[x1,x0] is non empty set
{x1,x0} is non empty set
{x1} is non empty trivial 1 -element set
{{x1,x0},{x1}} is non empty set
x1 is Element of the carrier of R
(f | ( the InternalRel of R -Seg x0)) . x1 is set
f . x1 is Element of c
(n | ( the InternalRel of R -Seg x0)) . x1 is set
n . x1 is Element of c
f . x0 is Element of c
f . (x0,(n | ( the InternalRel of R -Seg x0))) is set
[x0,(n | ( the InternalRel of R -Seg x0))] is non empty set
{x0,(n | ( the InternalRel of R -Seg x0))} is non empty set
{{x0,(n | ( the InternalRel of R -Seg x0))},{x0}} is non empty set
f . [x0,(n | ( the InternalRel of R -Seg x0))] is set
n . x0 is Element of c
R is RelStr
the carrier of R is set
[:NAT, the carrier of R:] is set
bool [:NAT, the carrier of R:] is non empty set
R is non empty RelStr
the carrier of R is non empty set
[:NAT, the carrier of R:] is non empty non finite set
bool [:NAT, the carrier of R:] is non empty non finite set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
Y is Relation-like NAT -defined the carrier of R -valued Function-like V23( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
dom Y is Element of bool NAT
rng Y is Element of bool the carrier of R
bool the carrier of R is non empty set
f is set
the InternalRel of R -Seg f is set
Coim ( the InternalRel of R,f) is set
{f} is non empty trivial 1 -element set
the InternalRel of R " {f} is set
(Coim ( the InternalRel of R,f)) \ {f} is Element of bool (Coim ( the InternalRel of R,f))
bool (Coim ( the InternalRel of R,f)) is non empty set
f is set
Y . f is set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of NAT
n + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of NAT
Y . (n + 1) is Element of the carrier of R
Y . n is Element of the carrier of R
[(Y . (n + 1)),(Y . n)] is non empty Element of [: the carrier of R, the carrier of R:]
{(Y . (n + 1)),(Y . n)} is non empty set
{(Y . (n + 1))} is non empty trivial 1 -element set
{{(Y . (n + 1)),(Y . n)},{(Y . (n + 1))}} is non empty set
the InternalRel of R -Seg (Y . n) is set
Coim ( the InternalRel of R,(Y . n)) is set
{(Y . n)} is non empty trivial 1 -element set
the InternalRel of R " {(Y . n)} is set
(Coim ( the InternalRel of R,(Y . n))) \ {(Y . n)} is Element of bool (Coim ( the InternalRel of R,(Y . n)))
bool (Coim ( the InternalRel of R,(Y . n))) is non empty set
Y is set
0 is empty trivial Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite cardinal {} -element Element of NAT
choose Y is Element of Y
f is Relation-like Function-like set
dom f is set
f . 0 is set
f is epsilon-transitive epsilon-connected ordinal natural finite cardinal set
f . f is set
the InternalRel of R -Seg (f . f) is set
Coim ( the InternalRel of R,(f . f)) is set
{(f . f)} is non empty trivial 1 -element set
the InternalRel of R " {(f . f)} is set
(Coim ( the InternalRel of R,(f . f))) \ {(f . f)} is Element of bool (Coim ( the InternalRel of R,(f . f)))
bool (Coim ( the InternalRel of R,(f . f))) is non empty set
( the InternalRel of R -Seg (f . f)) /\ Y is set
f + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of NAT
f . (f + 1) is set
choose (( the InternalRel of R -Seg (f . f)) /\ Y) is Element of ( the InternalRel of R -Seg (f . f)) /\ Y
rng f is set
f is set
n is set
f . n is set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of NAT
f . n is set
f is Relation-like NAT -defined the carrier of R -valued Function-like V23( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal set
f . n is Element of the carrier of R
the InternalRel of R -Seg (f . n) is set
Coim ( the InternalRel of R,(f . n)) is set
{(f . n)} is non empty trivial 1 -element set
the InternalRel of R " {(f . n)} is set
(Coim ( the InternalRel of R,(f . n))) \ {(f . n)} is Element of bool (Coim ( the InternalRel of R,(f . n)))
bool (Coim ( the InternalRel of R,(f . n))) is non empty set
( the InternalRel of R -Seg (f . n)) /\ Y is set
n + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of NAT
f . (n + 1) is Element of the carrier of R
choose (( the InternalRel of R -Seg (f . n)) /\ Y) is Element of ( the InternalRel of R -Seg (f . n)) /\ Y
[(f . (n + 1)),(f . n)] is non empty Element of [: the carrier of R, the carrier of R:]
{(f . (n + 1)),(f . n)} is non empty set
{(f . (n + 1))} is non empty trivial 1 -element set
{{(f . (n + 1)),(f . n)},{(f . (n + 1))}} is non empty set