:: RFUNCT_3 semantic presentation

K19(REAL) is V12() non finite set

COMPLEX is non empty V12() non finite complex-membered V80() set

K20(COMPLEX,COMPLEX) is V12() non finite complex-valued set
K19(K20(COMPLEX,COMPLEX)) is V12() non finite set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is V12() non finite complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V12() non finite set

K19(K20(REAL,REAL)) is V12() non finite set

K19(K20(K20(REAL,REAL),REAL)) is V12() non finite set

K19(K20(RAT,RAT)) is V12() non finite set

K19(K20(K20(RAT,RAT),RAT)) is V12() non finite set

K19(K20(INT,INT)) is V12() non finite set

K19(K20(K20(INT,INT),INT)) is V12() non finite set

K19(K20(K20(NAT,NAT),NAT)) is set

K19(omega) is V12() non finite set

K19(K20(NAT,REAL)) is V12() non finite set
K19(K19(REAL)) is V12() non finite set
K19(NAT) is V12() non finite set

K19(K20(COMPLEX,REAL)) is V12() non finite set
K101(NAT) is V27() set

Sum () is V36() real ext-real Element of REAL

K197() \$\$ () is V36() real ext-real Element of REAL

dom {} is set
rng {} is set
-infty is non empty non real ext-real non positive negative set
+infty is non empty non real ext-real positive non negative set
D is V36() real ext-real set
max (D,0) is V36() real ext-real set
- D is V36() real ext-real set
max ((- D),0) is V36() real ext-real set
D is V36() real ext-real set
(D) is V36() real ext-real Element of REAL
max (D,0) is V36() real ext-real set
(D) is V36() real ext-real Element of REAL
- D is V36() real ext-real set
max ((- D),0) is V36() real ext-real set
(D) - (D) is V36() real ext-real Element of REAL
D is V36() real ext-real set

(D) is V36() real ext-real Element of REAL
max (D,0) is V36() real ext-real set
(D) is V36() real ext-real Element of REAL
- D is V36() real ext-real set
max ((- D),0) is V36() real ext-real set
(D) + (D) is V36() real ext-real Element of REAL
D is V36() real ext-real set
(D) is V36() real ext-real Element of REAL
max (D,0) is V36() real ext-real set
2 * (D) is V36() real ext-real Element of REAL

D + (abs D) is V36() real ext-real Element of REAL
(D) is V36() real ext-real Element of REAL
- D is V36() real ext-real set
max ((- D),0) is V36() real ext-real set
(D) - (D) is V36() real ext-real Element of REAL
((D) - (D)) + (abs D) is V36() real ext-real Element of REAL
(D) + (D) is V36() real ext-real Element of REAL
((D) - (D)) + ((D) + (D)) is V36() real ext-real Element of REAL
D is V36() real ext-real set
F is V36() real ext-real set
D * F is V36() real ext-real set
((D * F)) is V36() real ext-real Element of REAL
max ((D * F),0) is V36() real ext-real set
(F) is V36() real ext-real Element of REAL
max (F,0) is V36() real ext-real set
D * (F) is V36() real ext-real Element of REAL
D is V36() real ext-real set
F is V36() real ext-real set
D + F is V36() real ext-real set
((D + F)) is V36() real ext-real Element of REAL
max ((D + F),0) is V36() real ext-real set
(D) is V36() real ext-real Element of REAL
max (D,0) is V36() real ext-real set
(F) is V36() real ext-real Element of REAL
max (F,0) is V36() real ext-real set
(D) + (F) is V36() real ext-real Element of REAL

F is non empty set

K20(NAT,F) is V12() non finite set
K19(K20(NAT,F)) is V12() non finite set

rng D is set
F is set
{F} is non empty V12() finite 1 -element set
D " {F} is set
(rng D) /\ {F} is finite set
the Element of (rng D) /\ {F} is Element of (rng D) /\ {F}
D is non empty set

K19(K20(D,REAL)) is V12() non finite set

X is V36() real ext-real set
Y is V36() real ext-real set
Y / X is V36() real ext-real Element of COMPLEX

F " {(Y / X)} is Element of K19(D)
K19(D) is set

(X (#) F) " {Y} is Element of K19(D)
fx is set
Y is Element of D
dom F is Element of K19(D)
dom (X (#) F) is Element of K19(D)
F . Y is V36() real ext-real Element of REAL
X * (F . Y) is V36() real ext-real Element of REAL
(X (#) F) . Y is V36() real ext-real Element of REAL
fx is set
Y is Element of D
dom (X (#) F) is Element of K19(D)
(X (#) F) . Y is V36() real ext-real Element of REAL
F . Y is V36() real ext-real Element of REAL
X * (F . Y) is V36() real ext-real Element of REAL
dom F is Element of K19(D)
D is non empty set

K19(K20(D,REAL)) is V12() non finite set

(0 (#) F) " is Element of K19(D)
K19(D) is set
dom F is Element of K19(D)
X is set
Y is Element of D
dom (0 (#) F) is Element of K19(D)
X is set
Y is Element of D
dom (0 (#) F) is Element of K19(D)
(0 (#) F) . Y is V36() real ext-real Element of REAL
F . Y is V36() real ext-real Element of REAL
0 * (F . Y) is V36() real ext-real Element of REAL
D is non empty set

K19(K20(D,REAL)) is V12() non finite set

X is V36() real ext-real Element of REAL

(abs F) " {X} is Element of K19(D)
K19(D) is set
- X is V36() real ext-real Element of REAL

F " {(- X),X} is Element of K19(D)
dom (abs F) is Element of K19(D)
dom F is Element of K19(D)
Y is set
fx is Element of D
(abs F) . fx is V36() real ext-real Element of REAL
F . fx is V36() real ext-real Element of REAL
abs (F . fx) is V36() real ext-real Element of REAL
- (F . fx) is V36() real ext-real Element of REAL
Y is set
fx is Element of D
F . fx is V36() real ext-real Element of REAL
- (F . fx) is V36() real ext-real Element of REAL
abs (- (F . fx)) is V36() real ext-real Element of REAL
abs (F . fx) is V36() real ext-real Element of REAL
(abs F) . fx is V36() real ext-real Element of REAL
abs (F . fx) is V36() real ext-real Element of REAL
(abs F) . fx is V36() real ext-real Element of REAL
D is non empty set

K19(K20(D,REAL)) is V12() non finite set

(abs F) " is Element of K19(D)
K19(D) is set
F " is Element of K19(D)
dom (abs F) is Element of K19(D)
dom F is Element of K19(D)
X is set
Y is Element of D
(abs F) . Y is V36() real ext-real Element of REAL
F . Y is V36() real ext-real Element of REAL
abs (F . Y) is V36() real ext-real Element of REAL
X is set
Y is Element of D
F . Y is V36() real ext-real Element of REAL
abs (F . Y) is V36() real ext-real Element of REAL
(abs F) . Y is V36() real ext-real Element of REAL
D is non empty set

K19(K20(D,REAL)) is V12() non finite set

X is V36() real ext-real Element of REAL

(abs F) " {X} is Element of K19(D)
K19(D) is set
the Element of (abs F) " {X} is Element of (abs F) " {X}
fx is Element of D
(abs F) . fx is V36() real ext-real Element of REAL
F . fx is V36() real ext-real Element of REAL
abs (F . fx) is V36() real ext-real Element of REAL
D is non empty set

K19(K20(D,REAL)) is V12() non finite set
F is non empty set

K19(K20(F,REAL)) is V12() non finite set

fx is V36() real ext-real Element of REAL

Y is V36() real ext-real Element of REAL
Y / fx is V36() real ext-real Element of REAL
Coim (X,(Y / fx)) is set

X " {(Y / fx)} is set
Coim ((fx (#) X),Y) is set

(fx (#) X) " {Y} is set
Coim (Y,(Y / fx)) is set
Y " {(Y / fx)} is set
Coim ((fx (#) Y),Y) is set
(fx (#) Y) " {Y} is set
card (Coim ((fx (#) X),Y)) is ordinal cardinal set
card (Coim ((fx (#) Y),Y)) is ordinal cardinal set
Y is V36() real ext-real Element of REAL
fx * Y is V36() real ext-real Element of REAL
(fx * Y) / fx is V36() real ext-real Element of REAL
{((fx * Y) / fx)} is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered set
Y " {((fx * Y) / fx)} is Element of K19(F)
K19(F) is set
Coim ((fx (#) Y),(fx * Y)) is set

(fx (#) Y) " {(fx * Y)} is set
X " {((fx * Y) / fx)} is Element of K19(D)
K19(D) is set
Coim ((fx (#) X),(fx * Y)) is set
(fx (#) X) " {(fx * Y)} is set
Coim (X,Y) is set

X " {Y} is set
card (Coim (X,Y)) is ordinal cardinal set
Coim (Y,Y) is set
Y " {Y} is set
card (Coim (Y,Y)) is ordinal cardinal set

D is non empty set

K19(K20(D,REAL)) is V12() non finite set
F is non empty set

K19(K20(F,REAL)) is V12() non finite set

- 1 is V36() real ext-real non positive set

- 1 is V36() real ext-real non positive Element of REAL

D is non empty set

K19(K20(D,REAL)) is V12() non finite set
F is non empty set

K19(K20(F,REAL)) is V12() non finite set

fx is V36() real ext-real Element of REAL

(abs X) " {fx} is Element of K19(D)
K19(D) is set
- fx is V36() real ext-real Element of REAL
{(- fx),fx} is non empty finite complex-membered ext-real-membered real-membered set
X " {(- fx),fx} is Element of K19(D)
(abs Y) " {fx} is Element of K19(F)
K19(F) is set
Y " {(- fx),fx} is Element of K19(F)
card ((abs X) " {fx}) is ordinal cardinal set
card ((abs Y) " {fx}) is ordinal cardinal set
fx is V36() real ext-real Element of REAL

(abs X) " {fx} is Element of K19(D)
K19(D) is set
X " {fx} is Element of K19(D)
(abs Y) " {fx} is Element of K19(F)
K19(F) is set
Y " {fx} is Element of K19(F)
card ((abs X) " {fx}) is ordinal cardinal set
card ((abs Y) " {fx}) is ordinal cardinal set
fx is V36() real ext-real Element of REAL

(abs X) " {fx} is Element of K19(D)
K19(D) is set
card ((abs X) " {fx}) is ordinal cardinal set
(abs Y) " {fx} is Element of K19(F)
K19(F) is set
card ((abs Y) " {fx}) is ordinal cardinal set
fx is V36() real ext-real Element of REAL

(abs X) " {fx} is Element of K19(D)
K19(D) is set
card ((abs X) " {fx}) is ordinal cardinal set
(abs Y) " {fx} is Element of K19(F)
K19(F) is set
card ((abs Y) " {fx}) is ordinal cardinal set
fx is V36() real ext-real Element of REAL

(abs X) " {fx} is Element of K19(D)
K19(D) is set
card ((abs X) " {fx}) is ordinal cardinal set
(abs Y) " {fx} is Element of K19(F)
K19(F) is set
card ((abs Y) " {fx}) is ordinal cardinal set
Coim ((abs X),fx) is set
(abs X) " {fx} is set
card (Coim ((abs X),fx)) is ordinal cardinal set
Coim ((abs Y),fx) is set
(abs Y) " {fx} is set
card (Coim ((abs Y),fx)) is ordinal cardinal set

D is set
F is set
K20(D,F) is set
K19(K20(D,F)) is set
X is Relation-like D -defined F -valued Function-like Element of K19(K20(D,F))

D is set
F is set
K20(D,F) is set
K19(K20(D,F)) is set
X is Relation-like D -defined F -valued Function-like Element of K19(K20(D,F))

D is set
F is set
PFuncs (D,F) is functional non empty set
K20(D,F) is set
K19(K20(D,F)) is set
X is Relation-like Function-like Element of PFuncs (D,F)
X is non empty (D,F)
K20(D,F) is set
K19(K20(D,F)) is set
Y is Element of X
D is non empty set
K19(D) is set
F is non empty set
X is Element of K19(D)
Y is Element of F
X --> Y is set
(D,F) is functional non empty (D,F)
X --> Y is Relation-like D -defined F -valued Function-like Element of K19(K20(D,F))
K20(D,F) is set
K19(K20(D,F)) is set
D is non empty set

(D,F) is functional non empty (D,F)
X is Relation-like D -defined F -valued Function-like (D,F,(D,F))
D is non empty set

(D,F) is functional non empty (D,F)

(D,REAL) is functional non empty (D, REAL )

K19(K20(D,F)) is set

K19(K20(D,REAL)) is V12() non finite set

- 1 is V36() real ext-real non positive set

K19(K20(D,F)) is set

K19(K20(D,REAL)) is V12() non finite set

fx + (- Y) is Relation-like Function-like set

K19(K20(D,F)) is set

K19(K20(D,REAL)) is V12() non finite set

K19(K20(D,F)) is set

K19(K20(D,REAL)) is V12() non finite set
D is non empty set

(D,F) is functional non empty (D,F)

(D,REAL) is functional non empty (D, REAL )

K19(K20(D,F)) is set

K19(K20(D,REAL)) is V12() non finite set

K19(K20(D,F)) is set

K19(K20(D,REAL)) is V12() non finite set

K19(K20(D,F)) is set

K19(K20(D,REAL)) is V12() non finite set
D is non empty set

(D,F) is functional non empty (D,F)

Y is V36() real ext-real set

(D,REAL) is functional non empty (D, REAL )

K19(K20(D,F)) is set

K19(K20(D,REAL)) is V12() non finite set
D is non empty set
(D,REAL) is functional non empty (D, REAL )
K20((D,REAL),(D,REAL)) is set
K20(K20((D,REAL),(D,REAL)),(D,REAL)) is set
K19(K20(K20((D,REAL),(D,REAL)),(D,REAL))) is set
F is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
F is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
X is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))

[Y,fx] is set
{Y,fx} is functional non empty finite set

{{Y,fx},{Y}} is non empty finite V51() set

D is non empty set
(D,REAL) is functional non empty (D, REAL )
(D) is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
K20((D,REAL),(D,REAL)) is set
K20(K20((D,REAL),(D,REAL)),(D,REAL)) is set
K19(K20(K20((D,REAL),(D,REAL)),(D,REAL))) is set

[F,X] is set
{F,X} is functional non empty finite set

{{F,X},{F}} is non empty finite V51() set
(D) . [F,X] is Relation-like Function-like set

[X,F] is set
{X,F} is functional non empty finite set

{{X,F},{X}} is non empty finite V51() set
(D) . [X,F] is Relation-like Function-like set

D is non empty set
(D,REAL) is functional non empty (D, REAL )
(D) is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
K20((D,REAL),(D,REAL)) is set
K20(K20((D,REAL),(D,REAL)),(D,REAL)) is set
K19(K20(K20((D,REAL),(D,REAL)),(D,REAL))) is set

[X,Y] is set
{X,Y} is functional non empty finite set

{{X,Y},{X}} is non empty finite V51() set
(D) . [X,Y] is Relation-like Function-like set
(D) . (F,((D) . (X,Y))) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)
[F,((D) . (X,Y))] is set
{F,((D) . (X,Y))} is functional non empty finite set

{{F,((D) . (X,Y))},{F}} is non empty finite V51() set
(D) . [F,((D) . (X,Y))] is Relation-like Function-like set

[F,X] is set
{F,X} is functional non empty finite set
{{F,X},{F}} is non empty finite V51() set
(D) . [F,X] is Relation-like Function-like set
(D) . (((D) . (F,X)),Y) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)
[((D) . (F,X)),Y] is set
{((D) . (F,X)),Y} is functional non empty finite set
{((D) . (F,X))} is functional non empty V12() finite 1 -element set
{{((D) . (F,X)),Y},{((D) . (F,X))}} is non empty finite V51() set
(D) . [((D) . (F,X)),Y] is Relation-like Function-like set

(D) . (F,((D) . (X,Y))) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)
[F,((D) . (X,Y))] is set
{F,((D) . (X,Y))} is functional non empty finite set
{{F,((D) . (X,Y))},{F}} is non empty finite V51() set
(D) . [F,((D) . (X,Y))] is Relation-like Function-like set

(D) . (F,(D,REAL,X,Y)) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)
[F,(D,REAL,X,Y)] is set
{F,(D,REAL,X,Y)} is functional non empty finite set
{{F,(D,REAL,X,Y)},{F}} is non empty finite V51() set
(D) . [F,(D,REAL,X,Y)] is Relation-like Function-like set
(D,REAL,F,(D,REAL,X,Y)) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))

(D,REAL,(D,REAL,F,X),Y) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))

(D,REAL,((D) . (F,X)),Y) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))
(D) . (((D) . (F,X)),Y) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)
[((D) . (F,X)),Y] is set
{((D) . (F,X)),Y} is functional non empty finite set
{((D) . (F,X))} is functional non empty V12() finite 1 -element set
{{((D) . (F,X)),Y},{((D) . (F,X))}} is non empty finite V51() set
(D) . [((D) . (F,X)),Y] is Relation-like Function-like set
D is non empty set
(D,REAL) is functional non empty (D, REAL )
[#] D is Element of K19(D)
K19(D) is set

(D) is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
K20((D,REAL),(D,REAL)) is set
K20(K20((D,REAL),(D,REAL)),(D,REAL)) is set
K19(K20(K20((D,REAL),(D,REAL)),(D,REAL))) is set
dom (D,REAL,([#] D),0) is Element of K19(D)
Y is Element of D

(D,REAL,X,(D,REAL,([#] D),0)) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))
dom (D,REAL,X,(D,REAL,([#] D),0)) is Element of K19(D)
(D,REAL,X,(D,REAL,([#] D),0)) . Y is V36() real ext-real Element of REAL
X . Y is V36() real ext-real Element of REAL
(D,REAL,([#] D),0) . Y is ordinal natural V36() real ext-real non negative V41() V42() finite cardinal Element of REAL
(X . Y) + ((D,REAL,([#] D),0) . Y) is V36() real ext-real Element of REAL
(X . Y) + 0 is V36() real ext-real Element of REAL
dom X is Element of K19(D)
(dom X) /\ D is Element of K19(D)
(D) . (X,(D,REAL,([#] D),0)) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)
[X,(D,REAL,([#] D),0)] is set
{X,(D,REAL,([#] D),0)} is functional non empty finite set

{{X,(D,REAL,([#] D),0)},{X}} is non empty finite V51() set
(D) . [X,(D,REAL,([#] D),0)] is Relation-like Function-like set
D is non empty set
(D,REAL) is functional non empty (D, REAL )
(D) is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
K20((D,REAL),(D,REAL)) is set
K20(K20((D,REAL),(D,REAL)),(D,REAL)) is set
K19(K20(K20((D,REAL),(D,REAL)),(D,REAL))) is set

[#] D is Element of K19(D)
K19(D) is set

D is non empty set
(D,REAL) is functional non empty (D, REAL )
(D) is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
K20((D,REAL),(D,REAL)) is set
K20(K20((D,REAL),(D,REAL)),(D,REAL)) is set
K19(K20(K20((D,REAL),(D,REAL)),(D,REAL))) is set
[#] D is Element of K19(D)
K19(D) is set

D is non empty set
(D,REAL) is functional non empty (D, REAL )

(D) is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
K20((D,REAL),(D,REAL)) is set
K20(K20((D,REAL),(D,REAL)),(D,REAL)) is set
K19(K20(K20((D,REAL),(D,REAL)),(D,REAL))) is set

D is non empty set
(D,REAL) is functional non empty (D, REAL )

(D) is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
K20((D,REAL),(D,REAL)) is set
K20(K20((D,REAL),(D,REAL)),(D,REAL)) is set
K19(K20(K20((D,REAL),(D,REAL)),(D,REAL))) is set

[#] D is Element of K19(D)
K19(D) is set

D is non empty set
(D,REAL) is functional non empty (D, REAL )

(D) is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
K20((D,REAL),(D,REAL)) is set
K20(K20((D,REAL),(D,REAL)),(D,REAL)) is set
K19(K20(K20((D,REAL),(D,REAL)),(D,REAL))) is set

(D,REAL,(D,F),X) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))
(D) . (((D) \$\$ F),X) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)
[((D) \$\$ F),X] is set
{((D) \$\$ F),X} is functional non empty finite set
{((D) \$\$ F)} is functional non empty V12() finite 1 -element set
{{((D) \$\$ F),X},{((D) \$\$ F)}} is non empty finite V51() set
(D) . [((D) \$\$ F),X] is Relation-like Function-like set
D is non empty set
(D,REAL) is functional non empty (D, REAL )

(D) is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
K20((D,REAL),(D,REAL)) is set
K20(K20((D,REAL),(D,REAL)),(D,REAL)) is set
K19(K20(K20((D,REAL),(D,REAL)),(D,REAL))) is set

(D,REAL,(D,F),(D,X)) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))
(D) . ((D,F),(D,X)) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)
[(D,F),(D,X)] is set
{(D,F),(D,X)} is functional non empty finite set
{(D,F)} is functional non empty V12() finite 1 -element set
{{(D,F),(D,X)},{(D,F)}} is non empty finite V51() set
(D) . [(D,F),(D,X)] is Relation-like Function-like set
D is non empty set
(D,REAL) is functional non empty (D, REAL )

(D) is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
K20((D,REAL),(D,REAL)) is set
K20(K20((D,REAL),(D,REAL)),(D,REAL)) is set
K19(K20(K20((D,REAL),(D,REAL)),(D,REAL))) is set

(D,REAL,X,(D,F)) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))

(D,REAL,(D,<*X*>),(D,F)) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))
D is non empty set
(D,REAL) is functional non empty (D, REAL )

(D) is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
K20((D,REAL),(D,REAL)) is set
K20(K20((D,REAL),(D,REAL)),(D,REAL)) is set
K19(K20(K20((D,REAL),(D,REAL)),(D,REAL))) is set

D is non empty set
(D,REAL) is functional non empty (D, REAL )

(D) is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
K20((D,REAL),(D,REAL)) is set
K20(K20((D,REAL),(D,REAL)),(D,REAL)) is set
K19(K20(K20((D,REAL),(D,REAL)),(D,REAL))) is set

(D,REAL,(D,REAL,F,X),Y) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))

(D,REAL,(D,<*F,X*>),Y) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))
D is non empty set
(D,REAL) is functional non empty (D, REAL )

(D) is Relation-like K20((D,REAL),(D,REAL)) -defined (D,REAL) -valued Function-like V18(K20((D,REAL),(D,REAL)),(D,REAL)) Element of K19(K20(K20((D,REAL),(D,REAL)),(D,REAL)))
K20((D,REAL),(D,REAL)) is set
K20(K20((D,REAL),(D,REAL)),(D,REAL)) is set
K19(K20(K20((D,REAL),(D,REAL)),(D,REAL))) is set

fx . (Y + 1) is Relation-like Function-like set
rng fx is functional finite Element of K19((D,REAL))
K19((D,REAL)) is set
rng Y is functional finite Element of K19((D,REAL))

(Y | xf) ^ (Y /^ xf) is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

xf - 1 is V36() real ext-real Element of REAL
max (0,(xf - 1)) is V36() real ext-real Element of REAL

(Y | xf) . xf is Relation-like Function-like set

((Y | xf) | x) ^ <*dr*> is Relation-like NAT -defined (D,REAL) -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of (D,REAL)
(Y | xf) | (Seg x) is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,(D,REAL)))
K20(NAT,(D,REAL)) is V12() non finite set
K19(K20(NAT,(D,REAL))) is V12() non finite set

(Y | (Seg xf)) | (Seg x) is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,(D,REAL)))

Y | ((Seg xf) /\ (Seg x)) is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,(D,REAL)))

x is set
Coim (fx,x) is finite set
{x} is non empty V12() finite 1 -element set
fx " {x} is finite set

Coim (Y,x) is finite set
Y " {x} is finite set

((Y | x) ^ <*dr*>) ^ (Y /^ xf) is Relation-like NAT -defined (D,REAL) -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

(card (((Y | x) ^ <*dr*>) " {x})) + (card ((Y /^ xf) " {x})) is ordinal natural V36() real ext-real non negative V41() V42() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

((card ((Y | x) " {x})) + (card (<*dr*> " {x}))) + (card ((Y /^ xf) " {x})) is ordinal natural V36() real ext-real non negative V41() V42() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

((card ((Y | x) " {x})) + (card ((Y /^ xf) " {x}))) + (card (<*dr*> " {x})) is ordinal natural V36() real ext-real non negative V41() V42() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(card (((Y | x) ^ (Y /^ xf)) " {x})) + (card (<*dr*> " {x})) is ordinal natural V36() real ext-real non negative V41() V42() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Coim ((fx | Y),x) is finite set
(fx | Y) " {x} is finite set

Coim (((Y | x) ^ (Y /^ xf)),x) is finite set
((Y | x) ^ (Y /^ xf)) " {x} is finite set

(D,(fx | Y)) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))

(D,((Y | x) ^ (Y /^ xf))) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))
(D) \$\$ ((Y | x) ^ (Y /^ xf)) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

(D,REAL,(D,((Y | x) ^ (Y /^ xf))),(D,<*dr*>)) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))

(D,(Y /^ xf)) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))
(D) \$\$ (Y /^ xf) is Relation-like Function-like complex-valued