:: 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

F

PFuncs (F

bool (PFuncs (F

[:F

bool [:F

R is functional Element of bool (PFuncs (F

c is Relation-like 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

union { b

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

union { b

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

union { b

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

{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

f is Element of bool the carrier of R

F

the carrier of F

F

the InternalRel of F

[: the carrier of F

bool [: the carrier of F

{ b

bool the carrier of F

Y is non empty Element of bool the carrier of F

f is set

the InternalRel of F

Coim ( the InternalRel of F

{f} is non empty trivial 1 -element set

the InternalRel of F

(Coim ( the InternalRel of F

bool (Coim ( the InternalRel of F

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

{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

Coim ( the InternalRel of F

{f} is non empty trivial 1 -element set

the InternalRel of F

(Coim ( the InternalRel of F

bool (Coim ( the InternalRel of F

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

the carrier of F

the InternalRel of F

[: the carrier of F

bool [: the carrier of F

{ b

Y is Element of the carrier of F

the InternalRel of F

Coim ( the InternalRel of F

{Y} is non empty trivial 1 -element set

the InternalRel of F

(Coim ( the InternalRel of F

bool (Coim ( the InternalRel of F

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

{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

Coim ( the InternalRel of F

{f} is non empty trivial 1 -element set

the InternalRel of F

(Coim ( the InternalRel of F

bool (Coim ( the InternalRel of F

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