:: RFUNCT_3 semantic presentation

REAL is non empty V12() non finite complex-membered ext-real-membered real-membered V80() set

NAT is V12() ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V80() Element of K19(REAL)

K19(REAL) is V12() non finite set

{} is Function-like functional empty ordinal natural V36() real ext-real non positive non negative finite V51() cardinal {} -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V80() FinSequence-membered set

the Function-like functional empty ordinal natural V36() real ext-real non positive non negative finite V51() cardinal {} -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V80() FinSequence-membered set is Function-like functional empty ordinal natural V36() real ext-real non positive non negative finite V51() cardinal {} -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V80() FinSequence-membered set

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

RAT is non empty V12() non finite complex-membered ext-real-membered real-membered rational-membered V80() set

INT is non empty V12() non finite complex-membered ext-real-membered real-membered rational-membered integer-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

K20(REAL,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

K20(K20(REAL,REAL),REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

K20(RAT,RAT) is RAT -valued V12() non finite complex-valued ext-real-valued real-valued set

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

K20(K20(RAT,RAT),RAT) is RAT -valued V12() non finite complex-valued ext-real-valued real-valued set

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

K20(INT,INT) is RAT -valued INT -valued V12() non finite complex-valued ext-real-valued real-valued set

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

K20(K20(INT,INT),INT) is RAT -valued INT -valued V12() non finite complex-valued ext-real-valued real-valued set

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

K20(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

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

omega is V12() ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V80() set

K19(omega) is V12() non finite set

K20(NAT,REAL) is V12() non finite complex-valued ext-real-valued real-valued 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

K20(COMPLEX,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

K101(NAT) is V27() set

1 is non empty ordinal natural V36() real ext-real positive non negative V41() V42() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

{{},1} is non empty finite V51() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

2 is non empty ordinal natural V36() real ext-real positive non negative V41() V42() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

3 is non empty ordinal natural V36() real ext-real positive non negative V41() V42() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

0 is Function-like functional empty ordinal natural V36() real ext-real non positive non negative V41() V42() finite V51() cardinal {} -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V80() FinSequence-membered Element of NAT

Seg 1 is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

{1} is non empty V12() finite V51() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

Seg 2 is non empty finite 2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

{1,2} is non empty finite V51() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

card {} is Function-like functional empty ordinal natural V36() real ext-real non positive non negative finite V51() cardinal {} -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V80() FinSequence-membered set

<*> REAL is Relation-like NAT -defined REAL -valued Function-like one-to-one constant functional empty ordinal natural V36() real ext-real non positive non negative finite finite-yielding V51() cardinal {} -element complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V80() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of REAL

Sum (<*> REAL) is V36() real ext-real Element of REAL

K197() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V18(K20(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(K20(REAL,REAL),REAL))

K197() $$ (<*> REAL) is V36() real ext-real Element of REAL

{0} is non empty V12() finite V51() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

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

abs D is V36() real ext-real Element of REAL

(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

abs 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

0 + 0 is Function-like functional empty ordinal natural V36() real ext-real non positive non negative V41() V42() finite V51() cardinal {} -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V80() FinSequence-membered Element of NAT

D 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

F is non empty set

X is Relation-like NAT -defined F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F

len 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

X | D is Relation-like NAT -defined F -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F

dom X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

Seg (len X) is finite len X -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

Seg D is finite D -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

X | (Seg D) is Relation-like NAT -defined F -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,F))

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

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

D is Relation-like Function-like 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

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

F is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

X is V36() real ext-real set

Y is V36() real ext-real set

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

{(Y / X)} is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered set

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

K19(D) is set

X (#) F is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

{Y} is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered 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

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

F is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

0 (#) F is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

(0 (#) F) " {0} 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

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

F is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

abs F is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

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

{X} is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered set

(abs F) " {X} is Element of K19(D)

K19(D) is set

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

{(- X),X} is non empty finite complex-membered ext-real-membered real-membered set

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

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

F is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

abs F is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

(abs F) " {0} is Element of K19(D)

K19(D) is set

F " {0} 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

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

F is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

abs F is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

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

{X} is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered set

(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

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

F is non empty set

K20(F,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

X is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

Y is Relation-like F -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(F,REAL))

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

fx (#) X is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

fx (#) Y is Relation-like F -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(F,REAL))

rng (fx (#) X) is complex-membered ext-real-membered real-membered Element of K19(REAL)

rng (fx (#) Y) is complex-membered ext-real-membered real-membered Element of K19(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

{(Y / fx)} is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered set

X " {(Y / fx)} is set

Coim ((fx (#) X),Y) is set

{Y} is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered 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)} is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered 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

{Y} is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered 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

rng X is complex-membered ext-real-membered real-membered Element of K19(REAL)

rng Y is complex-membered ext-real-membered real-membered Element of K19(REAL)

D is non empty set

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

F is non empty set

K20(F,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

X is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

- X is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

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

(- 1) (#) X is Relation-like Function-like set

Y is Relation-like F -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(F,REAL))

- Y is Relation-like F -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(F,REAL))

(- 1) (#) Y is Relation-like Function-like set

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

(- 1) (#) X is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

D is non empty set

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

F is non empty set

K20(F,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

X is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

abs X is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

Y is Relation-like F -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(F,REAL))

abs Y is Relation-like F -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(F,REAL))

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

{fx} is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered set

(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

{fx} is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered set

(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

{fx} is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered set

(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

{fx} is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered set

(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

{fx} is non empty V12() finite 1 -element complex-membered ext-real-membered real-membered set

(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

rng (abs X) is complex-membered ext-real-membered real-membered Element of K19(REAL)

rng (abs Y) is complex-membered ext-real-membered real-membered Element of K19(REAL)

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

{X} is functional non empty V12() finite 1 -element set

Y is Relation-like Function-like Element of {X}

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

{X} is functional non empty V12() finite 1 -element set

Y is Relation-like Function-like Element of {X}

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

F is complex-membered ext-real-membered real-membered 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

F is complex-membered ext-real-membered real-membered set

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

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

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

X + Y is Relation-like Function-like set

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

K20(D,F) is complex-valued ext-real-valued real-valued set

K19(K20(D,F)) is set

fx is Relation-like D -defined F -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,F))

Y is Relation-like D -defined F -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,F))

fx + Y is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

X - Y is Relation-like Function-like set

- Y is Relation-like Function-like complex-valued set

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

(- 1) (#) Y is Relation-like Function-like set

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

K20(D,F) is complex-valued ext-real-valued real-valued set

K19(K20(D,F)) is set

fx is Relation-like D -defined F -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,F))

Y is Relation-like D -defined F -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,F))

fx - Y is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

- Y is Relation-like Function-like complex-valued set

(- 1) (#) Y is Relation-like Function-like set

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

X (#) Y is Relation-like Function-like set

K20(D,F) is complex-valued ext-real-valued real-valued set

K19(K20(D,F)) is set

fx is Relation-like D -defined F -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,F))

Y is Relation-like D -defined F -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,F))

fx (#) Y is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

X / Y is Relation-like Function-like set

K20(D,F) is complex-valued ext-real-valued real-valued set

K19(K20(D,F)) is set

fx is Relation-like D -defined F -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,F))

Y is Relation-like D -defined F -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,F))

fx / Y is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

D is non empty set

F is complex-membered ext-real-membered real-membered set

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

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

|.X.| is Relation-like Function-like complex-valued ext-real-valued real-valued set

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

K20(D,F) is complex-valued ext-real-valued real-valued set

K19(K20(D,F)) is set

Y is Relation-like D -defined F -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,F))

abs Y is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

- X is Relation-like Function-like complex-valued set

(- 1) (#) X is Relation-like Function-like set

K20(D,F) is complex-valued ext-real-valued real-valued set

K19(K20(D,F)) is set

Y is Relation-like D -defined F -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,F))

- Y is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

(- 1) (#) Y is Relation-like Function-like set

X ^ is Relation-like Function-like set

K20(D,F) is complex-valued ext-real-valued real-valued set

K19(K20(D,F)) is set

Y is Relation-like D -defined F -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,F))

Y ^ is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued set

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

D is non empty set

F is complex-membered ext-real-membered real-membered set

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

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

Y is V36() real ext-real set

Y (#) X is Relation-like Function-like set

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

K20(D,F) is complex-valued ext-real-valued real-valued set

K19(K20(D,F)) is set

fx is Relation-like D -defined F -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,F))

Y (#) fx is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(D,REAL))

K20(D,REAL) is V12() non finite complex-valued ext-real-valued real-valued 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 is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))

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

F . (Y,fx) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

[Y,fx] is set

{Y,fx} is functional non empty finite set

{Y} is functional non empty V12() finite 1 -element set

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

F . [Y,fx] is Relation-like Function-like set

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

X . (Y,fx) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

X . [Y,fx] 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

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

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

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

[F,X] is set

{F,X} is functional non empty finite set

{F} is functional non empty V12() finite 1 -element set

{{F,X},{F}} is non empty finite V51() set

(D) . [F,X] is Relation-like Function-like set

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

[X,F] is set

{X,F} is functional non empty finite set

{X} is functional non empty V12() finite 1 -element set

{{X,F},{X}} is non empty finite V51() set

(D) . [X,F] is Relation-like Function-like set

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

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

(D) . (X,F) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (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

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

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

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

(D) . (X,Y) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

[X,Y] is set

{X,Y} is functional non empty finite set

{X} is functional non empty V12() finite 1 -element 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} is functional non empty V12() finite 1 -element 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,X) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

[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) . (X,Y) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

(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,REAL,X,Y) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))

(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,F,X) 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) . (F,X) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (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,REAL,([#] D),0) is Relation-like D -defined REAL -valued RAT -valued INT -valued Function-like complex-valued ext-real-valued real-valued natural-valued (D, REAL ,(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

dom (D,REAL,([#] D),0) is Element of K19(D)

Y is Element of D

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

(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} is functional non empty V12() finite 1 -element 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

the_unity_wrt (D) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

[#] D is Element of K19(D)

K19(D) is set

(D,REAL,([#] D),0) is Relation-like D -defined REAL -valued RAT -valued INT -valued Function-like complex-valued ext-real-valued real-valued natural-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 Element of K19(D)

K19(D) is set

(D,REAL,([#] D),0) is Relation-like D -defined REAL -valued RAT -valued INT -valued Function-like complex-valued ext-real-valued real-valued natural-valued (D, REAL ,(D,REAL))

D is non empty set

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

F is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (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) $$ F is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

D is non empty set

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

<*> (D,REAL) is Relation-like NAT -defined (D,REAL) -valued Function-like one-to-one constant functional empty ordinal natural V36() real ext-real non positive non negative finite finite-yielding V51() cardinal {} -element complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V80() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of (D,REAL)

(D,(<*> (D,REAL))) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(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) $$ (<*> (D,REAL)) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

[#] D is Element of K19(D)

K19(D) is set

(D,REAL,([#] D),0) is Relation-like D -defined REAL -valued RAT -valued INT -valued Function-like complex-valued ext-real-valued real-valued natural-valued (D, REAL ,(D,REAL))

the_unity_wrt (D) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

D is non empty set

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

F is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

(D,F) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(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) $$ F is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

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

<*X*> is Relation-like NAT -defined (D,REAL) -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

F ^ <*X*> is Relation-like NAT -defined (D,REAL) -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of (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) $$ (F ^ <*X*>) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

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

F is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

X is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

F ^ X is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (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) 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) $$ (F ^ X) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

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

(D) $$ F is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

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

(D) $$ X is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

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

F is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

(D,F) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(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) $$ F is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

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

<*X*> is Relation-like NAT -defined (D,REAL) -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

<*X*> ^ F is Relation-like NAT -defined (D,REAL) -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

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

(D) $$ (<*X*> ^ F) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

(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,<*X*>) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))

(D) $$ <*X*> is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (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 )

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

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

<*F,X*> is Relation-like NAT -defined (D,REAL) -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of (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) 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) $$ <*F,X*> is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

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

<*F*> is Relation-like NAT -defined (D,REAL) -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

<*X*> is Relation-like NAT -defined (D,REAL) -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

<*F*> ^ <*X*> is Relation-like NAT -defined (D,REAL) -valued Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

1 + 1 is non empty ordinal natural V36() real ext-real positive non negative V41() V42() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

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

(D) $$ (<*F*> ^ <*X*>) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

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

(D) $$ <*F*> is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

(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 is non empty set

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

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

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

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

<*F,X,Y*> is Relation-like NAT -defined (D,REAL) -valued Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like FinSequence of (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 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) $$ <*F,X,Y*> is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

(D,REAL,F,X) 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))

<*F,X*> is Relation-like NAT -defined (D,REAL) -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

<*Y*> is Relation-like NAT -defined (D,REAL) -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

<*F,X*> ^ <*Y*> is Relation-like NAT -defined (D,REAL) -valued Function-like non empty finite 2 + 1 -element FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

2 + 1 is non empty ordinal natural V36() real ext-real positive non negative V41() V42() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

(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) $$ (<*F,X*> ^ <*Y*>) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (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) $$ <*F,X*> is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (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 )

F is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

X is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

(D,F) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(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) $$ F is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

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

(D) $$ X is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

len F 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

Y 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

Y + 1 is non empty ordinal natural V36() real ext-real positive non negative V41() V42() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

fx is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

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

len fx 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

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

(D) $$ fx is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

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

(D) $$ Y is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (D,REAL)

0 + 1 is non empty ordinal natural V36() real ext-real positive non negative V41() V42() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

dom fx is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

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

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

dom Y is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

xf is ordinal natural V36() real ext-real non negative finite cardinal set

Y . xf is Relation-like Function-like set

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

Y /^ xf is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (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)

len Y 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

len (Y | xf) 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

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

<*dr*> is Relation-like NAT -defined (D,REAL) -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of (D,REAL)

(fx | Y) ^ <*dr*> is Relation-like NAT -defined (D,REAL) -valued Function-like non empty 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

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

x + 1 is non empty ordinal natural V36() real ext-real positive non negative V41() V42() finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT

Seg x is finite x -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

Seg xf is finite xf -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

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

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

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

(Seg xf) /\ (Seg x) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

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 x) is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,(D,REAL)))

Y | x is Relation-like NAT -defined (D,REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (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

card (Coim (fx,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 omega

Coim (Y,x) is finite set

Y " {x} is finite set

card (Coim (Y,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 omega

(fx | Y) " {x} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

card ((fx | Y) " {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 omega

<*dr*> " {x} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

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 omega

(card ((fx | Y) " {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

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

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

(((Y | x) ^ <*dr*>) ^ (Y /^ xf)) " {x} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

card ((((Y | x) ^ <*dr*>) ^ (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 omega

((Y | x) ^ <*dr*>) " {x} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

card (((Y | x) ^ <*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 omega

(Y /^ xf) " {x} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

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 omega

(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

(Y | x) " {x} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

card ((Y | x) " {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 omega

(card ((Y | x) " {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) " {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})) 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

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

((Y | x) ^ (Y /^ xf)) " {x} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

card (((Y | x) ^ (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 omega

(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

card (Coim ((fx | Y),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 omega

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

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

card (Coim (((Y | x) ^ (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 omega

len (fx | Y) 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

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

(D) $$ (fx | Y) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (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,<*dr*>) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))

(D) $$ <*dr*> 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 | x)) is Relation-like D -defined REAL -valued Function-like complex-valued ext-real-valued real-valued (D, REAL ,(D,REAL))

(D) $$ (Y | x) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of (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