:: WELLFND1 semantic presentation

REAL is set

bool REAL is non empty set

bool NAT is non empty non finite set

RAT is set
INT is set
bool NAT is non empty non finite set

{{},1} is non empty 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

c is set
r is set
F1() is set
F2() is set
PFuncs (F1(),F2()) is non empty functional M14(F1(),F2())
bool (PFuncs (F1(),F2())) is non empty set
[:F1(),F2():] is set
bool [:F1(),F2():] is non empty set
R is functional Element of bool (PFuncs (F1(),F2()))
c is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
R is set

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

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

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
{ b1 where b1 is Element of bool the carrier of R : ( b1 is (R) & b1 is lower ) } is set
union { b1 where b1 is Element of bool the carrier of R : ( b1 is (R) & b1 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
{ b1 where b1 is Element of bool the carrier of R : ( b1 is (R) & b1 is lower ) } is set
union { b1 where b1 is Element of bool the carrier of R : ( b1 is (R) & b1 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
{ b1 where b1 is Element of bool the carrier of R : ( b1 is (R) & b1 is lower ) } is set
union { b1 where b1 is Element of bool the carrier of R : ( b1 is (R) & b1 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
{ b1 where b1 is Element of bool the carrier of R : ( b1 is (R) & b1 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 { b1 where b1 is Element of bool the carrier of R : ( b1 is (R) & b1 is lower ) } is set
f is Element of bool the carrier of R
F1() is non empty RelStr
the carrier of F1() is non empty set
F2() is Element of the carrier of F1()
the InternalRel of F1() is Relation-like the carrier of F1() -defined the carrier of F1() -valued Element of bool [: the carrier of F1(), the carrier of F1():]
[: the carrier of F1(), the carrier of F1():] is non empty set
bool [: the carrier of F1(), the carrier of F1():] is non empty set
{ b1 where b1 is Element of the carrier of F1() : P1[b1] } is set
bool the carrier of F1() is non empty set
Y is non empty Element of bool the carrier of F1()
f is set
the InternalRel of F1() -Seg f is set
Coim ( the InternalRel of F1(),f) is set
{f} is non empty trivial 1 -element set
the InternalRel of F1() " {f} is set
(Coim ( the InternalRel of F1(),f)) \ {f} is Element of bool (Coim ( the InternalRel of F1(),f))
bool (Coim ( the InternalRel of F1(),f)) is non empty set
f is Element of the carrier of F1()
n is Element of the carrier of F1()
n is Element of the carrier of F1()
[n,f] is non empty Element of [: the carrier of F1(), the carrier of F1():]
{n,f} is non empty set
{n} is non empty trivial 1 -element set
{{n,f},{n}} is non empty set
the InternalRel of F1() -Seg f is set
Coim ( the InternalRel of F1(),f) is set
{f} is non empty trivial 1 -element set
the InternalRel of F1() " {f} is set
(Coim ( the InternalRel of F1(),f)) \ {f} is Element of bool (Coim ( the InternalRel of F1(),f))
bool (Coim ( the InternalRel of F1(),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
F1() is non empty RelStr
the carrier of F1() is non empty set
the InternalRel of F1() is Relation-like the carrier of F1() -defined the carrier of F1() -valued Element of bool [: the carrier of F1(), the carrier of F1():]
[: the carrier of F1(), the carrier of F1():] is non empty set
bool [: the carrier of F1(), the carrier of F1():] is non empty set
{ b1 where b1 is Element of the carrier of F1() : P1[b1] } is set
Y is Element of the carrier of F1()
the InternalRel of F1() -Seg Y is set
Coim ( the InternalRel of F1(),Y) is set
{Y} is non empty trivial 1 -element set
the InternalRel of F1() " {Y} is set
(Coim ( the InternalRel of F1(),Y)) \ {Y} is Element of bool (Coim ( the InternalRel of F1(),Y))
bool (Coim ( the InternalRel of F1(),Y)) is non empty set
f is Element of the carrier of F1()
f is Element of the carrier of F1()
[f,f] is non empty Element of [: the carrier of F1(), the carrier of F1():]
{f,f} is non empty set
{f} is non empty trivial 1 -element set
{{f,f},{f}} is non empty set
the InternalRel of F1() -Seg f is set
Coim ( the InternalRel of F1(),f) is set
{f} is non empty trivial 1 -element set
the InternalRel of F1() " {f} is set
(Coim ( the InternalRel of F1(),f)) \ {f} is Element of bool (Coim ( the InternalRel of F1(),f))
bool (Coim ( the InternalRel of F1(),f)) is non empty set
n is Element of the carrier of F1()
Y is Element of the carrier of F1()
f is Element of the carrier of F1()
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

NAT +` (card the carrier of R) is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal set

PFuncs ( the carrier of R,()) 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,())
rng n is Element of bool ()
bool () is non empty non finite set

dom n is Element of bool the carrier of R
bool the carrier of R is non empty set

[: the carrier of R,(PFuncs ( the carrier of R,())):] is non empty set
[:[: the carrier of R,(PFuncs ( the carrier of R,())):],():] is non empty non finite set
bool [:[: the carrier of R,(PFuncs ( the carrier of R,())):],():] is non empty non finite set
f is Relation-like [: the carrier of R,(PFuncs ( the carrier of R,())):] -defined nextcard Y -valued Function-like V23([: the carrier of R,(PFuncs ( the carrier of R,())):], nextcard Y) Element of bool [:[: the carrier of R,(PFuncs ( the carrier of R,())):],():]
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))

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

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

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

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,():] is non empty non finite set
bool [: the carrier of R,():] 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,():]
n is set
n .: n is Element of bool ()
bool () is non empty non finite 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,():]

x1 is Relation-like the carrier of R -defined nextcard Y -valued Function-like Element of PFuncs ( the carrier of R,())

[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 ()

n . gr is 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

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

choose Y is Element of Y

dom f is set
f . 0 is 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 . (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

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

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

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