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