:: TIETZE semantic presentation

REAL is non empty V34() V77() V78() V79() V83() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V77() V78() V79() V80() V81() V82() V83() Element of K10(REAL)
K10(REAL) is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal V77() V78() V79() V80() V81() V82() V83() set
K10(omega) is non empty set
K11(NAT,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11(NAT,REAL)) is non empty set
K10(K10(REAL)) is non empty set
COMPLEX is non empty V34() V77() V83() set
K10(NAT) is non empty set
RAT is non empty V34() V77() V78() V79() V80() V83() set
INT is non empty V34() V77() V78() V79() V80() V81() V83() set
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
K11(1,1) is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K10(K11(1,1)) is non empty set
K11(K11(1,1),1) is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K10(K11(K11(1,1),1)) is non empty set
K11(K11(1,1),REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11(K11(1,1),REAL)) is non empty set
K11(REAL,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K11(K11(REAL,REAL),REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11(K11(REAL,REAL),REAL)) is non empty set
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
K11(2,2) is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K11(K11(2,2),REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11(K11(2,2),REAL)) is non empty set
K10(K11(REAL,REAL)) is non empty set
K432(2) is V188() L15()
the carrier of K432(2) is set
K503() is non empty strict TopSpace-like V209() TopStruct
the carrier of K503() is non empty V77() V78() V79() set
RealSpace is non empty strict Reflexive discerning V179() triangle Discerning V209() MetrStruct
R^1 is non empty strict TopSpace-like V209() TopStruct
K510() is non empty strict TopSpace-like V209() SubSpace of R^1
K488(K510(),K510()) is non empty strict TopSpace-like TopStruct
the carrier of K488(K510(),K510()) is non empty set
K512() is non empty strict TopSpace-like V209() V211() SubSpace of R^1
the carrier of K512() is non empty V77() V78() V79() set
K10( the carrier of K512()) is non empty set
K10(K10( the carrier of K512())) is non empty set
K521(2) is non empty V212() SubSpace of K432(2)
the carrier of K521(2) is non empty set
K11( the carrier of K512(), the carrier of K521(2)) is non empty Relation-like set
K10(K11( the carrier of K512(), the carrier of K521(2))) is non empty set
K525() is non empty Relation-like the carrier of K512() -defined the carrier of K512() -defined the carrier of K521(2) -valued the carrier of K521(2) -valued Function-like total total quasi_total quasi_total onto continuous Element of K10(K11( the carrier of K512(), the carrier of K521(2)))
K522() is Element of the carrier of K521(2)
K524(K522()) is non empty strict open SubSpace of K521(2)
the carrier of K524(K522()) is non empty set
0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional real V60() V61() V66() complex-valued ext-real-valued real-valued natural-valued V77() V78() V79() V80() V81() V82() V83() Function-yielding V231() Element of NAT
the empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional real V60() complex-valued ext-real-valued real-valued natural-valued V77() V78() V79() V80() V81() V82() V83() Function-yielding V231() set is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional real V60() complex-valued ext-real-valued real-valued natural-valued V77() V78() V79() V80() V81() V82() V83() Function-yielding V231() set
].0,1.[ is non empty V77() V78() V79() Element of K10(REAL)
R^1 ].0,1.[ is non empty V77() V78() V79() Element of K10( the carrier of K512())
K512() | (R^1 ].0,1.[) is non empty strict TopSpace-like V209() SubSpace of K512()
the carrier of (K512() | (R^1 ].0,1.[)) is non empty V77() V78() V79() set
K11( the carrier of K524(K522()), the carrier of (K512() | (R^1 ].0,1.[))) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of K524(K522()), the carrier of (K512() | (R^1 ].0,1.[)))) is non empty set
K523() is Element of the carrier of K521(2)
K524(K523()) is non empty strict open SubSpace of K521(2)
the carrier of K524(K523()) is non empty set
1 / 2 is ext-real non negative real V60() Element of REAL
3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
3 / 2 is ext-real non negative real V60() Element of REAL
].(1 / 2),(3 / 2).[ is non empty V77() V78() V79() Element of K10(REAL)
R^1 ].(1 / 2),(3 / 2).[ is non empty V77() V78() V79() Element of K10( the carrier of K512())
K512() | (R^1 ].(1 / 2),(3 / 2).[) is non empty strict TopSpace-like V209() SubSpace of K512()
the carrier of (K512() | (R^1 ].(1 / 2),(3 / 2).[)) is non empty V77() V78() V79() set
K11( the carrier of K524(K523()), the carrier of (K512() | (R^1 ].(1 / 2),(3 / 2).[))) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of K524(K523()), the carrier of (K512() | (R^1 ].(1 / 2),(3 / 2).[)))) is non empty set
{} is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional real V60() complex-valued ext-real-valued real-valued natural-valued V77() V78() V79() V80() V81() V82() V83() Function-yielding V231() set
{{},1} is non empty V77() V78() V79() V80() V81() V82() set
ExtREAL is non empty V78() set
K11( the carrier of K432(2),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of K432(2),REAL)) is non empty set
K10( the carrier of K432(2)) is non empty set
K680() is set
{{}} is non empty functional V77() V78() V79() V80() V81() V82() set
K381({{}}) is M15({{}})
K11(K381({{}}),{{}}) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K10(K11(K381({{}}),{{}})) is non empty set
PFuncs (K381({{}}),{{}}) is set
the carrier of R^1 is non empty V77() V78() V79() set
the carrier of RealSpace is non empty V77() V78() V79() set
K613(RealSpace) is TopStruct
real_dist is non empty Relation-like K11(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(K11(REAL,REAL),REAL))
MetrStruct(# REAL,real_dist #) is strict MetrStruct
-infty is non empty ext-real non positive negative non real set
+infty is non empty ext-real positive non negative non real set
T is ext-real real V60() set
f2 is ext-real real V60() set
T - f2 is ext-real real V60() set
|.(T - f2).| is ext-real real V60() Element of REAL
f1 is ext-real real V60() set
f2 - f1 is ext-real real V60() set
f2 + f1 is ext-real real V60() set
0 + f2 is ext-real real V60() set
- (T - f2) is ext-real real V60() set
f2 - T is ext-real real V60() set
0 + T is ext-real real V60() set
T is Relation-like Function-like complex-valued ext-real-valued real-valued set
f2 is Relation-like Function-like complex-valued ext-real-valued real-valued set
f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
f1 - T is Relation-like Function-like complex-valued ext-real-valued real-valued set
f1 - f2 is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom (f1 - f2) is set
dom f1 is set
dom f2 is set
(dom f1) /\ (dom f2) is set
dom (f1 - T) is set
dom T is set
(dom f1) /\ (dom T) is set
C is set
(f1 - T) . C is ext-real real V60() Element of REAL
f1 . C is ext-real real V60() Element of REAL
T . C is ext-real real V60() Element of REAL
(f1 . C) - (T . C) is ext-real real V60() Element of REAL
f2 . C is ext-real real V60() Element of REAL
(f1 . C) - (f2 . C) is ext-real real V60() Element of REAL
(f1 - f2) . C is ext-real real V60() Element of REAL
T is Relation-like Function-like complex-valued ext-real-valued real-valued set
f2 is Relation-like Function-like complex-valued ext-real-valued real-valued set
f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
T - f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
f2 - f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom (T - f1) is set
dom T is set
dom f1 is set
(dom T) /\ (dom f1) is set
dom (f2 - f1) is set
dom f2 is set
(dom f2) /\ (dom f1) is set
C is set
(T - f1) . C is ext-real real V60() Element of REAL
T . C is ext-real real V60() Element of REAL
f1 . C is ext-real real V60() Element of REAL
(T . C) - (f1 . C) is ext-real real V60() Element of REAL
f2 . C is ext-real real V60() Element of REAL
(f2 . C) - (f1 . C) is ext-real real V60() Element of REAL
(f2 - f1) . C is ext-real real V60() Element of REAL
NAT --> 0 is non empty Relation-like NAT -defined NAT -valued RAT -valued INT -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued natural-valued Function-yielding V231() Element of K10(K11(NAT,NAT))
K11(NAT,NAT) is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K10(K11(NAT,NAT)) is non empty set
f2 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
f1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
f2 . f1 is ext-real real V60() Element of REAL
T is empty V96() V97() {} -element TopSpace-like T_0 TopStruct
the carrier of T is empty V2() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional V34() real V60() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V77() V78() V79() V80() V81() V82() V83() Function-yielding V231() set
f2 is TopSpace-like TopStruct
the carrier of f2 is set
K11( the carrier of T, the carrier of f2) is Relation-like set
K10(K11( the carrier of T, the carrier of f2)) is non empty set
f1 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding the carrier of T -defined the carrier of f2 -valued Function-like one-to-one constant functional total quasi_total real V60() complex-valued ext-real-valued real-valued natural-valued V77() V78() V79() V80() V81() V82() V83() Function-yielding V231() Element of K10(K11( the carrier of T, the carrier of f2))
K10( the carrier of f2) is non empty set
C is Element of K10( the carrier of f2)
f1 " C is empty V2() non proper ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional real V60() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V77() V78() V79() V80() V81() V82() V83() closed Function-yielding V231() Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
T is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued summable Element of K10(K11(NAT,REAL))
f2 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued summable Element of K10(K11(NAT,REAL))
Sum T is ext-real real V60() Element of REAL
Sum f2 is ext-real real V60() Element of REAL
Partial_Sums T is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
lim (Partial_Sums T) is ext-real real V60() Element of REAL
Partial_Sums f2 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
lim (Partial_Sums f2) is ext-real real V60() Element of REAL
f1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
(Partial_Sums T) . f1 is ext-real real V60() Element of REAL
(Partial_Sums f2) . f1 is ext-real real V60() Element of REAL
T is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
Sum T is ext-real real V60() Element of REAL
abs (Sum T) is ext-real real V60() Element of REAL
abs T is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
Sum (abs T) is ext-real real V60() Element of REAL
Partial_Sums T is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
abs (Partial_Sums T) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
Partial_Sums (abs T) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
f2 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
(abs (Partial_Sums T)) . f2 is ext-real real V60() Element of REAL
(Partial_Sums (abs T)) . f2 is ext-real real V60() Element of REAL
(Partial_Sums T) . f2 is ext-real real V60() Element of REAL
|.((Partial_Sums T) . f2).| is ext-real real V60() Element of REAL
f2 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
T . (f2 + 1) is ext-real real V60() Element of REAL
((Partial_Sums T) . f2) + (T . (f2 + 1)) is ext-real real V60() Element of REAL
|.(((Partial_Sums T) . f2) + (T . (f2 + 1))).| is ext-real real V60() Element of REAL
|.(T . (f2 + 1)).| is ext-real real V60() Element of REAL
|.((Partial_Sums T) . f2).| + |.(T . (f2 + 1)).| is ext-real real V60() Element of REAL
((Partial_Sums (abs T)) . f2) + |.(T . (f2 + 1)).| is ext-real real V60() Element of REAL
(Partial_Sums T) . (f2 + 1) is ext-real real V60() Element of REAL
|.((Partial_Sums T) . (f2 + 1)).| is ext-real real V60() Element of REAL
(abs (Partial_Sums T)) . (f2 + 1) is ext-real real V60() Element of REAL
(abs T) . (f2 + 1) is ext-real real V60() Element of REAL
((Partial_Sums (abs T)) . f2) + ((abs T) . (f2 + 1)) is ext-real real V60() Element of REAL
(Partial_Sums (abs T)) . (f2 + 1) is ext-real real V60() Element of REAL
(abs (Partial_Sums T)) . 0 is ext-real real V60() Element of REAL
(Partial_Sums T) . 0 is ext-real real V60() Element of REAL
abs ((Partial_Sums T) . 0) is ext-real real V60() Element of REAL
T . 0 is ext-real real V60() Element of REAL
abs (T . 0) is ext-real real V60() Element of REAL
(abs T) . 0 is ext-real real V60() Element of REAL
(Partial_Sums (abs T)) . 0 is ext-real real V60() Element of REAL
lim (abs (Partial_Sums T)) is ext-real real V60() Element of REAL
lim (Partial_Sums (abs T)) is ext-real real V60() Element of REAL
lim (Partial_Sums T) is ext-real real V60() Element of REAL
abs (lim (Partial_Sums T)) is ext-real real V60() Element of REAL
T is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
lim T is ext-real real V60() Element of REAL
f1 is non empty ext-real positive non negative real V60() set
f2 is non empty ext-real positive non negative real V60() set
1 - f1 is ext-real real V60() Element of REAL
T . 0 is ext-real real V60() Element of REAL
C is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
C . 0 is ext-real real V60() Element of REAL
D is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
D + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
T . (D + 1) is ext-real real V60() Element of REAL
T . D is ext-real real V60() Element of REAL
(T . (D + 1)) - (T . D) is ext-real real V60() Element of REAL
((T . (D + 1)) - (T . D)) + (T . D) is ext-real real V60() Element of REAL
C . (D + 1) is ext-real real V60() Element of REAL
(T . D) + (C . (D + 1)) is ext-real real V60() Element of REAL
Partial_Sums C is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
abs C is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
D is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
(abs C) . D is ext-real real V60() Element of REAL
C . D is ext-real real V60() Element of REAL
abs (C . D) is ext-real real V60() Element of REAL
|.f1.| is ext-real real V60() Element of REAL
f1 GeoSeq is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
D is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
g2 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() set
1 + g2 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
C . D is ext-real real V60() Element of REAL
C . g2 is ext-real real V60() Element of REAL
g2 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
T . (g2 + 1) is ext-real real V60() Element of REAL
T . g2 is ext-real real V60() Element of REAL
(T . (g2 + 1)) - (T . g2) is ext-real real V60() Element of REAL
(abs C) . D is ext-real real V60() Element of REAL
T . D is ext-real real V60() Element of REAL
(T . D) - (T . g2) is ext-real real V60() Element of REAL
|.((T . D) - (T . g2)).| is ext-real real V60() Element of REAL
(T . g2) - (T . D) is ext-real real V60() Element of REAL
|.((T . g2) - (T . D)).| is ext-real real V60() Element of REAL
f1 to_power g2 is ext-real real V60() set
f2 * (f1 to_power g2) is ext-real real V60() set
f2 * 1 is ext-real non negative real V60() Element of REAL
(f2 * 1) * (f1 to_power g2) is ext-real real V60() Element of REAL
f1 " is non empty ext-real positive non negative real V60() set
(f1 ") * f1 is ext-real non negative real V60() set
f2 * ((f1 ") * f1) is ext-real non negative real V60() set
(f2 * ((f1 ") * f1)) * (f1 to_power g2) is ext-real real V60() set
f2 * (f1 ") is ext-real non negative real V60() set
f1 * (f1 to_power g2) is ext-real real V60() set
(f2 * (f1 ")) * (f1 * (f1 to_power g2)) is ext-real real V60() set
f1 to_power 1 is ext-real real V60() set
(f1 to_power 1) * (f1 to_power g2) is ext-real real V60() set
(f2 * (f1 ")) * ((f1 to_power 1) * (f1 to_power g2)) is ext-real real V60() set
f1 to_power D is ext-real real V60() set
(f2 * (f1 ")) * (f1 to_power D) is ext-real real V60() set
f1 |^ D is ext-real real V60() set
(f2 * (f1 ")) * (f1 |^ D) is ext-real real V60() set
(f1 GeoSeq) . D is ext-real real V60() Element of REAL
(f2 * (f1 ")) * ((f1 GeoSeq) . D) is ext-real real V60() Element of REAL
(f2 * (f1 ")) (#) (f1 GeoSeq) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
((f2 * (f1 ")) (#) (f1 GeoSeq)) . D is ext-real real V60() Element of REAL
D is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() set
T . D is ext-real real V60() Element of REAL
(lim T) - (T . D) is ext-real real V60() Element of REAL
|.((lim T) - (T . D)).| is ext-real real V60() Element of REAL
f1 to_power D is ext-real real V60() set
f2 * (f1 to_power D) is ext-real real V60() set
(f2 * (f1 to_power D)) / (1 - f1) is ext-real real V60() Element of REAL
g1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
g1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
C ^\ (g1 + 1) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of C
abs (C ^\ (g1 + 1)) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
g2 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
(abs (C ^\ (g1 + 1))) . g2 is ext-real real V60() Element of REAL
(C ^\ (g1 + 1)) . g2 is ext-real real V60() Element of REAL
|.((C ^\ (g1 + 1)) . g2).| is ext-real real V60() Element of REAL
(g1 + 1) + g2 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
C . ((g1 + 1) + g2) is ext-real real V60() Element of REAL
|.(C . ((g1 + 1) + g2)).| is ext-real real V60() Element of REAL
g1 + g2 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
(g1 + g2) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
T . ((g1 + g2) + 1) is ext-real real V60() Element of REAL
T . (g1 + g2) is ext-real real V60() Element of REAL
(T . ((g1 + g2) + 1)) - (T . (g1 + g2)) is ext-real real V60() Element of REAL
|.((T . ((g1 + g2) + 1)) - (T . (g1 + g2))).| is ext-real real V60() Element of REAL
(T . (g1 + g2)) - (T . ((g1 + g2) + 1)) is ext-real real V60() Element of REAL
|.((T . (g1 + g2)) - (T . ((g1 + g2) + 1))).| is ext-real real V60() Element of REAL
f1 to_power (g1 + g2) is ext-real real V60() set
f2 * (f1 to_power (g1 + g2)) is ext-real real V60() set
f1 to_power g1 is ext-real real V60() set
f1 to_power g2 is ext-real real V60() set
(f1 to_power g1) * (f1 to_power g2) is ext-real real V60() set
f2 * ((f1 to_power g1) * (f1 to_power g2)) is ext-real real V60() set
f2 * (f1 to_power g1) is ext-real real V60() set
(f2 * (f1 to_power g1)) * (f1 to_power g2) is ext-real real V60() set
f1 |^ g2 is ext-real real V60() set
(f2 * (f1 to_power g1)) * (f1 |^ g2) is ext-real real V60() set
(f1 GeoSeq) . g2 is ext-real real V60() Element of REAL
(f2 * (f1 to_power g1)) * ((f1 GeoSeq) . g2) is ext-real real V60() Element of REAL
(f2 * (f1 to_power D)) (#) (f1 GeoSeq) is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
((f2 * (f1 to_power D)) (#) (f1 GeoSeq)) . g2 is ext-real real V60() Element of REAL
Sum C is ext-real real V60() Element of REAL
Sum (C ^\ (g1 + 1)) is ext-real real V60() Element of REAL
(T . D) + (Sum (C ^\ (g1 + 1))) is ext-real real V60() Element of REAL
Sum (abs (C ^\ (g1 + 1))) is ext-real real V60() Element of REAL
Sum ((f2 * (f1 to_power D)) (#) (f1 GeoSeq)) is ext-real real V60() Element of REAL
Sum (f1 GeoSeq) is ext-real real V60() Element of REAL
(f2 * (f1 to_power D)) * (Sum (f1 GeoSeq)) is ext-real real V60() Element of REAL
1 / (1 - f1) is ext-real real V60() Element of REAL
(f2 * (f1 to_power D)) * (1 / (1 - f1)) is ext-real real V60() Element of REAL
T is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
T . 0 is ext-real real V60() Element of REAL
lim T is ext-real real V60() Element of REAL
f1 is non empty ext-real positive non negative real V60() set
f2 is non empty ext-real positive non negative real V60() set
1 - f1 is ext-real real V60() Element of REAL
f2 / (1 - f1) is ext-real real V60() Element of REAL
(T . 0) - (f2 / (1 - f1)) is ext-real real V60() Element of REAL
(T . 0) + (f2 / (1 - f1)) is ext-real real V60() Element of REAL
f1 to_power 0 is ext-real real V60() set
(lim T) - (T . 0) is ext-real real V60() Element of REAL
|.((lim T) - (T . 0)).| is ext-real real V60() Element of REAL
f2 * 1 is ext-real non negative real V60() Element of REAL
(f2 * 1) / (1 - f1) is ext-real real V60() Element of REAL
T is non empty set
PFuncs (T,REAL) is set
K11(NAT,(PFuncs (T,REAL))) is Relation-like set
K10(K11(NAT,(PFuncs (T,REAL)))) is non empty set
f2 is non empty set
f1 is Relation-like NAT -defined PFuncs (T,REAL) -valued Function-like quasi_total Element of K10(K11(NAT,(PFuncs (T,REAL))))
lim (f1,f2) is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
K11(T,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11(T,REAL)) is non empty set
f1 . 0 is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
dom (f1 . 0) is Element of K10(T)
K10(T) is non empty set
C is non empty Element of K10(T)
g1 is non empty ext-real positive non negative real V60() set
D is non empty ext-real positive non negative real V60() set
1 - g1 is ext-real real V60() Element of REAL
K11(C,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11(C,REAL)) is non empty set
g2 is non empty Relation-like C -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(C,REAL))
f is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
dom f is Element of K10(T)
h is ext-real real V60() Element of REAL
h * (1 - g1) is ext-real real V60() Element of REAL
(h * (1 - g1)) / D is ext-real real V60() Element of REAL
log (g1,((h * (1 - g1)) / D)) is ext-real real V60() set
1 + (log (g1,((h * (1 - g1)) / D))) is ext-real real V60() Element of REAL
g is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
D * ((h * (1 - g1)) / D) is ext-real real V60() Element of REAL
D / D is ext-real non negative real V60() Element of COMPLEX
(h * (1 - g1)) * (D / D) is ext-real real V60() Element of REAL
g1 to_power (log (g1,((h * (1 - g1)) / D))) is ext-real real V60() set
g1 to_power g is ext-real real V60() set
D * (g1 to_power g) is ext-real real V60() set
(h * (1 - g1)) / (1 - g1) is ext-real real V60() Element of REAL
(D * (g1 to_power g)) / (1 - g1) is ext-real real V60() Element of REAL
F is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
f1 . F is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
c₁₂ is Element of T
(f1 . F) . c₁₂ is ext-real real V60() Element of REAL
f . c₁₂ is ext-real real V60() Element of REAL
((f1 . F) . c₁₂) - (f . c₁₂) is ext-real real V60() Element of REAL
abs (((f1 . F) . c₁₂) - (f . c₁₂)) is ext-real real V60() Element of REAL
f1 # c₁₂ is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
(f1 # c₁₂) . F is ext-real real V60() Element of REAL
|.(((f1 . F) . c₁₂) - (f . c₁₂)).| is ext-real real V60() Element of REAL
(f . c₁₂) - ((f1 . F) . c₁₂) is ext-real real V60() Element of REAL
|.((f . c₁₂) - ((f1 . F) . c₁₂)).| is ext-real real V60() Element of REAL
F is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() set
(f1 # c₁₂) . F is ext-real real V60() Element of REAL
f1 . F is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
(f1 . F) . c₁₂ is ext-real real V60() Element of REAL
F + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
f1 . (F + 1) is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
dom (f1 . (F + 1)) is Element of K10(T)
dom (f1 . F) is Element of K10(T)
(dom (f1 . F)) /\ (dom (f1 . (F + 1))) is Element of K10(T)
(f1 . F) - (f1 . (F + 1)) is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
dom ((f1 . F) - (f1 . (F + 1))) is Element of K10(T)
((f1 . F) - (f1 . (F + 1))) . c₁₂ is ext-real real V60() Element of REAL
(f1 . (F + 1)) . c₁₂ is ext-real real V60() Element of REAL
((f1 . F) . c₁₂) - ((f1 . (F + 1)) . c₁₂) is ext-real real V60() Element of REAL
f2 /\ (dom ((f1 . F) - (f1 . (F + 1)))) is Element of K10(T)
g1 to_power F is ext-real real V60() set
D * (g1 to_power F) is ext-real real V60() set
|.(((f1 . F) . c₁₂) - ((f1 . (F + 1)) . c₁₂)).| is ext-real real V60() Element of REAL
(f1 # c₁₂) . (F + 1) is ext-real real V60() Element of REAL
((f1 # c₁₂) . F) - ((f1 # c₁₂) . (F + 1)) is ext-real real V60() Element of REAL
|.(((f1 # c₁₂) . F) - ((f1 # c₁₂) . (F + 1))).| is ext-real real V60() Element of REAL
lim (f1 # c₁₂) is ext-real real V60() Element of REAL
(lim (f1 # c₁₂)) - ((f1 # c₁₂) . F) is ext-real real V60() Element of REAL
|.((lim (f1 # c₁₂)) - ((f1 # c₁₂) . F)).| is ext-real real V60() Element of REAL
g1 to_power F is ext-real real V60() set
D * (g1 to_power F) is ext-real real V60() set
(D * (g1 to_power F)) / (1 - g1) is ext-real real V60() Element of REAL
1 - 1 is ext-real real V60() Element of REAL
h is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() set
f1 . h is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
(lim (f1,f2)) - (f1 . h) is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
g1 to_power h is ext-real real V60() set
D * (g1 to_power h) is ext-real real V60() set
(D * (g1 to_power h)) / (1 - g1) is ext-real real V60() Element of REAL
g is set
dom ((lim (f1,f2)) - (f1 . h)) is set
f2 /\ (dom ((lim (f1,f2)) - (f1 . h))) is set
((lim (f1,f2)) - (f1 . h)) . g is ext-real real V60() Element of REAL
abs (((lim (f1,f2)) - (f1 . h)) . g) is ext-real real V60() Element of REAL
dom ((lim (f1,f2)) - (f1 . h)) is Element of K10(T)
f2 /\ (dom ((lim (f1,f2)) - (f1 . h))) is Element of K10(T)
c₁₂ is Element of T
f1 # c₁₂ is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
F is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() set
F + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
(f1 # c₁₂) . (F + 1) is ext-real real V60() Element of REAL
f1 . (F + 1) is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
(f1 . (F + 1)) . c₁₂ is ext-real real V60() Element of REAL
dom (f1 . (F + 1)) is Element of K10(T)
f1 . F is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
dom (f1 . F) is Element of K10(T)
(dom (f1 . F)) /\ (dom (f1 . (F + 1))) is Element of K10(T)
(f1 . F) - (f1 . (F + 1)) is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
dom ((f1 . F) - (f1 . (F + 1))) is Element of K10(T)
f2 /\ (dom ((f1 . F) - (f1 . (F + 1)))) is Element of K10(T)
g1 to_power F is ext-real real V60() set
D * (g1 to_power F) is ext-real real V60() set
(f1 # c₁₂) . F is ext-real real V60() Element of REAL
(f1 . F) . c₁₂ is ext-real real V60() Element of REAL
((f1 . F) - (f1 . (F + 1))) . c₁₂ is ext-real real V60() Element of REAL
((f1 # c₁₂) . F) - ((f1 # c₁₂) . (F + 1)) is ext-real real V60() Element of REAL
|.(((f1 # c₁₂) . F) - ((f1 # c₁₂) . (F + 1))).| is ext-real real V60() Element of REAL
lim (f1 # c₁₂) is ext-real real V60() Element of REAL
F is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
(f1 # c₁₂) . F is ext-real real V60() Element of REAL
(lim (f1 # c₁₂)) - ((f1 # c₁₂) . F) is ext-real real V60() Element of REAL
|.((lim (f1 # c₁₂)) - ((f1 # c₁₂) . F)).| is ext-real real V60() Element of REAL
g1 to_power F is ext-real real V60() set
D * (g1 to_power F) is ext-real real V60() set
(D * (g1 to_power F)) / (1 - g1) is ext-real real V60() Element of REAL
dom (lim (f1,f2)) is Element of K10(T)
(lim (f1,f2)) . c₁₂ is ext-real real V60() Element of REAL
((lim (f1,f2)) . c₁₂) - ((f1 # c₁₂) . F) is ext-real real V60() Element of REAL
|.(((lim (f1,f2)) . c₁₂) - ((f1 # c₁₂) . F)).| is ext-real real V60() Element of REAL
f1 . F is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
(f1 . F) . c₁₂ is ext-real real V60() Element of REAL
((lim (f1,f2)) . c₁₂) - ((f1 . F) . c₁₂) is ext-real real V60() Element of REAL
|.(((lim (f1,f2)) . c₁₂) - ((f1 . F) . c₁₂)).| is ext-real real V60() Element of REAL
T is non empty set
PFuncs (T,REAL) is set
K11(NAT,(PFuncs (T,REAL))) is Relation-like set
K10(K11(NAT,(PFuncs (T,REAL)))) is non empty set
f2 is non empty set
f1 is Relation-like NAT -defined PFuncs (T,REAL) -valued Function-like quasi_total Element of K10(K11(NAT,(PFuncs (T,REAL))))
f1 . 0 is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
K11(T,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11(T,REAL)) is non empty set
lim (f1,f2) is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
D is non empty ext-real positive non negative real V60() set
C is non empty ext-real positive non negative real V60() set
1 - D is ext-real real V60() Element of REAL
C / (1 - D) is ext-real real V60() Element of REAL
dom (lim (f1,f2)) is Element of K10(T)
K10(T) is non empty set
D to_power 0 is ext-real real V60() set
(lim (f1,f2)) - (f1 . 0) is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
C * 1 is ext-real non negative real V60() Element of REAL
(C * 1) / (1 - D) is ext-real real V60() Element of REAL
g1 is Element of f2
(f1 . 0) . g1 is ext-real real V60() Element of REAL
((f1 . 0) . g1) - (C / (1 - D)) is ext-real real V60() Element of REAL
(lim (f1,f2)) . g1 is ext-real real V60() Element of REAL
((f1 . 0) . g1) + (C / (1 - D)) is ext-real real V60() Element of REAL
dom (f1 . 0) is Element of K10(T)
(dom (lim (f1,f2))) /\ (dom (f1 . 0)) is Element of K10(T)
dom ((lim (f1,f2)) - (f1 . 0)) is Element of K10(T)
f2 /\ (dom ((lim (f1,f2)) - (f1 . 0))) is Element of K10(T)
((lim (f1,f2)) - (f1 . 0)) . g1 is ext-real real V60() Element of REAL
|.(((lim (f1,f2)) - (f1 . 0)) . g1).| is ext-real real V60() Element of REAL
((lim (f1,f2)) . g1) - ((f1 . 0) . g1) is ext-real real V60() Element of REAL
|.(((lim (f1,f2)) . g1) - ((f1 . 0) . g1)).| is ext-real real V60() Element of REAL
T is non empty set
PFuncs (T,REAL) is set
K11(NAT,(PFuncs (T,REAL))) is Relation-like set
K10(K11(NAT,(PFuncs (T,REAL)))) is non empty set
f2 is non empty set
K11(f2,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11(f2,REAL)) is non empty set
f1 is Relation-like NAT -defined PFuncs (T,REAL) -valued Function-like quasi_total Element of K10(K11(NAT,(PFuncs (T,REAL))))
lim (f1,f2) is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
K11(T,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11(T,REAL)) is non empty set
D is non empty ext-real positive non negative real V60() set
C is non empty ext-real positive non negative real V60() set
g1 is non empty Relation-like f2 -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(f2,REAL))
dom g1 is non empty Element of K10(f2)
K10(f2) is non empty set
f1 . 0 is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
dom (f1 . 0) is Element of K10(T)
K10(T) is non empty set
f is Element of T
h is ext-real real V60() Element of REAL
1 - D is ext-real real V60() Element of REAL
h * (1 - D) is ext-real real V60() Element of REAL
(h * (1 - D)) / C is ext-real real V60() Element of REAL
log (D,((h * (1 - D)) / C)) is ext-real real V60() set
1 + (log (D,((h * (1 - D)) / C))) is ext-real real V60() Element of REAL
g is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
D to_power (log (D,((h * (1 - D)) / C))) is ext-real real V60() set
D to_power g is ext-real real V60() set
C * ((h * (1 - D)) / C) is ext-real real V60() Element of REAL
C / C is ext-real non negative real V60() Element of COMPLEX
(h * (1 - D)) * (C / C) is ext-real real V60() Element of REAL
C * (D to_power g) is ext-real real V60() set
(h * (1 - D)) / (1 - D) is ext-real real V60() Element of REAL
(C * (D to_power g)) / (1 - D) is ext-real real V60() Element of REAL
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
f1 . c₁₂ is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
dom (f1 . c₁₂) is Element of K10(T)
(dom (f1 . c₁₂)) /\ (dom g1) is Element of K10(f2)
(f1 . c₁₂) - g1 is Relation-like f2 -defined Function-like complex-valued ext-real-valued real-valued set
dom ((f1 . c₁₂) - g1) is Element of K10(f2)
((f1 . c₁₂) - g1) . f is ext-real real V60() Element of REAL
(f1 . c₁₂) . f is ext-real real V60() Element of REAL
g1 . f is ext-real real V60() Element of REAL
((f1 . c₁₂) . f) - (g1 . f) is ext-real real V60() Element of REAL
F is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
D to_power c₁₂ is ext-real real V60() set
D to_power F is ext-real real V60() set
C * (D to_power c₁₂) is ext-real real V60() set
C * (D to_power F) is ext-real real V60() set
(C * (D to_power c₁₂)) * (1 - D) is ext-real real V60() Element of REAL
(C * (D to_power c₁₂)) * 1 is ext-real real V60() Element of REAL
(C * (D to_power c₁₂)) / 1 is ext-real real V60() Element of REAL
(C * (D to_power c₁₂)) / (1 - D) is ext-real real V60() Element of REAL
1 - 1 is ext-real real V60() Element of REAL
(C * (D to_power F)) / (1 - D) is ext-real real V60() Element of REAL
f2 /\ (dom ((f1 . c₁₂) - g1)) is Element of K10(f2)
|.(((f1 . c₁₂) . f) - (g1 . f)).| is ext-real real V60() Element of REAL
g2 is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
g2 . f is ext-real real V60() Element of REAL
((f1 . c₁₂) . f) - (g2 . f) is ext-real real V60() Element of REAL
abs (((f1 . c₁₂) . f) - (g2 . f)) is ext-real real V60() Element of REAL
dom g2 is Element of K10(T)
f is Element of T
h is ext-real real V60() Element of REAL
g2 . f is ext-real real V60() Element of REAL
f is Element of T
dom g2 is Element of K10(T)
f1 # f is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
g2 . f is ext-real real V60() Element of REAL
h is ext-real real V60() set
g is ext-real real V60() Element of REAL
F is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
(f1 # f) . c₁₂ is ext-real real V60() Element of REAL
((f1 # f) . c₁₂) - (g2 . f) is ext-real real V60() Element of REAL
abs (((f1 # f) . c₁₂) - (g2 . f)) is ext-real real V60() Element of REAL
f1 . c₁₂ is Relation-like T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11(T,REAL))
(f1 . c₁₂) . f is ext-real real V60() Element of REAL
lim (f1 # f) is ext-real real V60() Element of REAL
T is TopSpace-like TopStruct
the carrier of T is set
K10( the carrier of T) is non empty set
f2 is closed Element of K10( the carrier of T)
T | f2 is strict TopSpace-like SubSpace of T
f1 is Element of K10( the carrier of T)
the carrier of (T | f2) is set
T is non empty TopSpace-like TopStruct
f2 is non empty TopSpace-like TopStruct
the carrier of f2 is non empty set
the carrier of T is non empty set
f1 is non empty TopSpace-like SubSpace of T
the carrier of f1 is non empty set
K11( the carrier of f1, the carrier of f2) is non empty Relation-like set
K10(K11( the carrier of f1, the carrier of f2)) is non empty set
C is non empty TopSpace-like SubSpace of T
the carrier of C is non empty set
K11( the carrier of C, the carrier of f2) is non empty Relation-like set
K10(K11( the carrier of C, the carrier of f2)) is non empty set
f1 meet C is non empty strict TopSpace-like SubSpace of T
the carrier of (f1 meet C) is non empty set
D is non empty Relation-like the carrier of f1 -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of f1, the carrier of f2))
D | (f1 meet C) is non empty Relation-like the carrier of (f1 meet C) -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (f1 meet C), the carrier of f2))
K11( the carrier of (f1 meet C), the carrier of f2) is non empty Relation-like set
K10(K11( the carrier of (f1 meet C), the carrier of f2)) is non empty set
g1 is non empty Relation-like the carrier of C -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of C, the carrier of f2))
g1 | (f1 meet C) is non empty Relation-like the carrier of (f1 meet C) -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (f1 meet C), the carrier of f2))
D union g1 is non empty Relation-like the carrier of (f1 union C) -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (f1 union C), the carrier of f2))
f1 union C is non empty strict TopSpace-like SubSpace of T
the carrier of (f1 union C) is non empty set
K11( the carrier of (f1 union C), the carrier of f2) is non empty Relation-like set
K10(K11( the carrier of (f1 union C), the carrier of f2)) is non empty set
g2 is Element of the carrier of T
(D union g1) . g2 is set
D . g2 is set
g1 . g2 is set
(D union g1) | the carrier of f1 is Relation-like the carrier of f1 -defined the carrier of (f1 union C) -defined the carrier of f2 -valued Function-like Element of K10(K11( the carrier of (f1 union C), the carrier of f2))
((D union g1) | the carrier of f1) . g2 is set
(D union g1) | f1 is non empty Relation-like the carrier of f1 -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of f1, the carrier of f2))
((D union g1) | f1) . g2 is set
(D union g1) | the carrier of C is Relation-like the carrier of C -defined the carrier of (f1 union C) -defined the carrier of f2 -valued Function-like Element of K10(K11( the carrier of (f1 union C), the carrier of f2))
((D union g1) | the carrier of C) . g2 is set
(D union g1) | C is non empty Relation-like the carrier of C -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of C, the carrier of f2))
((D union g1) | C) . g2 is set
T is non empty TopSpace-like TopStruct
f2 is non empty TopSpace-like TopStruct
the carrier of f2 is non empty set
f1 is non empty TopSpace-like SubSpace of T
the carrier of f1 is non empty set
K11( the carrier of f1, the carrier of f2) is non empty Relation-like set
K10(K11( the carrier of f1, the carrier of f2)) is non empty set
C is non empty TopSpace-like SubSpace of T
the carrier of C is non empty set
K11( the carrier of C, the carrier of f2) is non empty Relation-like set
K10(K11( the carrier of C, the carrier of f2)) is non empty set
f1 meet C is non empty strict TopSpace-like SubSpace of T
the carrier of (f1 meet C) is non empty set
D is non empty Relation-like the carrier of f1 -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of f1, the carrier of f2))
D | (f1 meet C) is non empty Relation-like the carrier of (f1 meet C) -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (f1 meet C), the carrier of f2))
K11( the carrier of (f1 meet C), the carrier of f2) is non empty Relation-like set
K10(K11( the carrier of (f1 meet C), the carrier of f2)) is non empty set
rng D is non empty Element of K10( the carrier of f2)
K10( the carrier of f2) is non empty set
g1 is non empty Relation-like the carrier of C -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of C, the carrier of f2))
g1 | (f1 meet C) is non empty Relation-like the carrier of (f1 meet C) -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (f1 meet C), the carrier of f2))
D union g1 is non empty Relation-like the carrier of (f1 union C) -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (f1 union C), the carrier of f2))
f1 union C is non empty strict TopSpace-like SubSpace of T
the carrier of (f1 union C) is non empty set
K11( the carrier of (f1 union C), the carrier of f2) is non empty Relation-like set
K10(K11( the carrier of (f1 union C), the carrier of f2)) is non empty set
rng (D union g1) is non empty Element of K10( the carrier of f2)
rng g1 is non empty Element of K10( the carrier of f2)
(rng D) \/ (rng g1) is non empty Element of K10( the carrier of f2)
the carrier of f1 \/ the carrier of C is non empty set
dom g1 is non empty Element of K10( the carrier of C)
K10( the carrier of C) is non empty set
f is set
dom D is non empty Element of K10( the carrier of f1)
K10( the carrier of f1) is non empty set
dom (D union g1) is non empty Element of K10( the carrier of (f1 union C))
K10( the carrier of (f1 union C)) is non empty set
h is set
(D union g1) . h is set
the carrier of T is non empty set
D . h is set
g1 . h is set
T is non empty TopSpace-like TopStruct
f2 is non empty TopSpace-like TopStruct
the carrier of f2 is non empty set
f1 is non empty TopSpace-like SubSpace of T
the carrier of f1 is non empty set
K11( the carrier of f1, the carrier of f2) is non empty Relation-like set
K10(K11( the carrier of f1, the carrier of f2)) is non empty set
C is non empty TopSpace-like SubSpace of T
the carrier of C is non empty set
K11( the carrier of C, the carrier of f2) is non empty Relation-like set
K10(K11( the carrier of C, the carrier of f2)) is non empty set
f1 meet C is non empty strict TopSpace-like SubSpace of T
the carrier of (f1 meet C) is non empty set
K10( the carrier of f1) is non empty set
f1 union C is non empty strict TopSpace-like SubSpace of T
the carrier of (f1 union C) is non empty set
K10( the carrier of C) is non empty set
D is non empty Relation-like the carrier of f1 -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of f1, the carrier of f2))
D | (f1 meet C) is non empty Relation-like the carrier of (f1 meet C) -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (f1 meet C), the carrier of f2))
K11( the carrier of (f1 meet C), the carrier of f2) is non empty Relation-like set
K10(K11( the carrier of (f1 meet C), the carrier of f2)) is non empty set
g1 is non empty Relation-like the carrier of C -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of C, the carrier of f2))
g1 | (f1 meet C) is non empty Relation-like the carrier of (f1 meet C) -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (f1 meet C), the carrier of f2))
D union g1 is non empty Relation-like the carrier of (f1 union C) -defined the carrier of f2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (f1 union C), the carrier of f2))
K11( the carrier of (f1 union C), the carrier of f2) is non empty Relation-like set
K10(K11( the carrier of (f1 union C), the carrier of f2)) is non empty set
the carrier of f1 \/ the carrier of C is non empty set
f is Element of K10( the carrier of f1)
(D union g1) .: f is Element of K10( the carrier of f2)
K10( the carrier of f2) is non empty set
D .: f is Element of K10( the carrier of f2)
h is set
g is Element of the carrier of (f1 union C)
(D union g1) . g is Element of the carrier of f2
the carrier of T is non empty set
D . g is set
h is set
g is Element of the carrier of f1
D . g is Element of the carrier of f2
(D union g1) . g is set
f is Element of K10( the carrier of C)
(D union g1) .: f is Element of K10( the carrier of f2)
g1 .: f is Element of K10( the carrier of f2)
h is set
g is Element of the carrier of (f1 union C)
(D union g1) . g is Element of the carrier of f2
the carrier of T is non empty set
g1 . g is set
h is set
g is Element of the carrier of C
g1 . g is Element of the carrier of f2
(D union g1) . g is set
T is ext-real real V60() set
f2 is set
f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
C is Relation-like Function-like complex-valued ext-real-valued real-valued set
D is set
dom f1 is set
f2 /\ (dom f1) is set
f1 . D is ext-real real V60() Element of REAL
abs (f1 . D) is ext-real real V60() Element of REAL
dom C is set
f2 /\ (dom C) is set
C . D is ext-real real V60() Element of REAL
abs (C . D) is ext-real real V60() Element of REAL
T is ext-real real V60() set
f2 is set
f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom f1 is set
f1 | f2 is Relation-like Function-like complex-valued ext-real-valued real-valued set
C is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom C is set
C | f2 is Relation-like Function-like complex-valued ext-real-valued real-valued set
D is set
f2 /\ (dom C) is set
C . D is ext-real real V60() Element of REAL
abs (C . D) is ext-real real V60() Element of REAL
f1 . D is ext-real real V60() Element of REAL
(f1 | f2) . D is ext-real real V60() Element of REAL
f2 /\ (dom f1) is set
T is ext-real real V60() set
T / 3 is ext-real real V60() Element of REAL
2 * T is ext-real real V60() Element of REAL
(2 * T) / 3 is ext-real real V60() Element of REAL
f2 is non empty TopSpace-like TopStruct
the carrier of f2 is non empty set
K10( the carrier of f2) is non empty set
K11( the carrier of f2, the carrier of R^1) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of f2, the carrier of R^1)) is non empty set
f1 is closed Element of K10( the carrier of f2)
f2 | f1 is strict TopSpace-like closed SubSpace of f2
the carrier of (f2 | f1) is set
K11( the carrier of (f2 | f1), the carrier of R^1) is Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of (f2 | f1), the carrier of R^1)) is non empty set
right_closed_halfline (T / 3) is V77() V78() V79() closed Element of K10(REAL)
K349((T / 3),+infty) is set
R^1 (right_closed_halfline (T / 3)) is V77() V78() V79() closed Element of K10( the carrier of K512())
- (T / 3) is ext-real real V60() Element of REAL
left_closed_halfline (- (T / 3)) is V77() V78() V79() closed Element of K10(REAL)
K350(-infty,(- (T / 3))) is set
R^1 (left_closed_halfline (- (T / 3))) is V77() V78() V79() closed Element of K10( the carrier of K512())
f is Relation-like the carrier of (f2 | f1) -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of (f2 | f1), the carrier of R^1))
dom f is Element of K10( the carrier of (f2 | f1))
K10( the carrier of (f2 | f1)) is non empty set
f1 /\ (dom f) is Element of K10( the carrier of (f2 | f1))
h is ext-real real V60() Element of REAL
2 * h is ext-real real V60() Element of REAL
(2 * h) / 3 is ext-real real V60() Element of REAL
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V209() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (0,1)) is non empty V77() V78() V79() set
((2 * h) / 3) * 0 is ext-real real V60() Element of REAL
h / 3 is ext-real real V60() Element of REAL
- (h / 3) is ext-real real V60() Element of REAL
(((2 * h) / 3) * 0) + (- (h / 3)) is ext-real real V60() Element of REAL
((2 * h) / 3) * 1 is ext-real real V60() Element of REAL
(((2 * h) / 3) * 1) + (- (h / 3)) is ext-real real V60() Element of REAL
Closed-Interval-TSpace (((((2 * h) / 3) * 0) + (- (h / 3))),((((2 * h) / 3) * 1) + (- (h / 3)))) is non empty strict TopSpace-like V209() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (((((2 * h) / 3) * 0) + (- (h / 3))),((((2 * h) / 3) * 1) + (- (h / 3))))) is non empty V77() V78() V79() set
K11( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (((((2 * h) / 3) * 0) + (- (h / 3))),((((2 * h) / 3) * 1) + (- (h / 3)))))) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (((((2 * h) / 3) * 0) + (- (h / 3))),((((2 * h) / 3) * 1) + (- (h / 3))))))) is non empty set
[.0,1.] is V77() V78() V79() Element of K10(REAL)
F is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (((((2 * h) / 3) * 0) + (- (h / 3))),((((2 * h) / 3) * 1) + (- (h / 3))))) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (((((2 * h) / 3) * 0) + (- (h / 3))),((((2 * h) / 3) * 1) + (- (h / 3)))))))
f " (R^1 (left_closed_halfline (- (T / 3)))) is Element of K10( the carrier of (f2 | f1))
f " (R^1 (right_closed_halfline (T / 3))) is Element of K10( the carrier of (f2 | f1))
- (- (T / 3)) is ext-real real V60() Element of REAL
f " (left_closed_halfline (- (T / 3))) is Element of K10( the carrier of (f2 | f1))
f " (right_closed_halfline (T / 3)) is Element of K10( the carrier of (f2 | f1))
c₁₂ is closed Element of K10( the carrier of f2)
F is closed Element of K10( the carrier of f2)
E2 is non empty Relation-like the carrier of f2 -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of f2, the carrier of R^1))
rng E2 is non empty V77() V78() V79() Element of K10( the carrier of R^1)
K10( the carrier of R^1) is non empty set
g1 is set
dom E2 is non empty Element of K10( the carrier of f2)
h is set
E2 . h is ext-real real V60() Element of REAL
K11( the carrier of f2, the carrier of (Closed-Interval-TSpace (0,1))) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of f2, the carrier of (Closed-Interval-TSpace (0,1)))) is non empty set
Closed-Interval-TSpace ((- (T / 3)),(T / 3)) is non empty strict TopSpace-like V209() SubSpace of R^1
the carrier of (Closed-Interval-TSpace ((- (T / 3)),(T / 3))) is non empty V77() V78() V79() set
[.(- (T / 3)),(T / 3).] is V77() V78() V79() Element of K10(REAL)
F * E2 is Relation-like the carrier of f2 -defined the carrier of (Closed-Interval-TSpace (((((2 * h) / 3) * 0) + (- (h / 3))),((((2 * h) / 3) * 1) + (- (h / 3))))) -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of f2, the carrier of (Closed-Interval-TSpace (((((2 * h) / 3) * 0) + (- (h / 3))),((((2 * h) / 3) * 1) + (- (h / 3)))))))
K11( the carrier of f2, the carrier of (Closed-Interval-TSpace (((((2 * h) / 3) * 0) + (- (h / 3))),((((2 * h) / 3) * 1) + (- (h / 3)))))) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of f2, the carrier of (Closed-Interval-TSpace (((((2 * h) / 3) * 0) + (- (h / 3))),((((2 * h) / 3) * 1) + (- (h / 3))))))) is non empty set
rng (F * E2) is V77() V78() V79() Element of K10( the carrier of (Closed-Interval-TSpace (((((2 * h) / 3) * 0) + (- (h / 3))),((((2 * h) / 3) * 1) + (- (h / 3))))))
K10( the carrier of (Closed-Interval-TSpace (((((2 * h) / 3) * 0) + (- (h / 3))),((((2 * h) / 3) * 1) + (- (h / 3)))))) is non empty set
dom E2 is non empty Element of K10( the carrier of f2)
dom F is non empty V77() V78() V79() Element of K10( the carrier of (Closed-Interval-TSpace (0,1)))
K10( the carrier of (Closed-Interval-TSpace (0,1))) is non empty set
dom (F * E2) is Element of K10( the carrier of f2)
K11( the carrier of f2, the carrier of (Closed-Interval-TSpace ((- (T / 3)),(T / 3)))) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of f2, the carrier of (Closed-Interval-TSpace ((- (T / 3)),(T / 3))))) is non empty set
h is non empty Relation-like the carrier of f2 -defined the carrier of (Closed-Interval-TSpace ((- (T / 3)),(T / 3))) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of f2, the carrier of (Closed-Interval-TSpace ((- (T / 3)),(T / 3)))))
g1 is non empty Relation-like the carrier of f2 -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of f2, the carrier of (Closed-Interval-TSpace (0,1))))
z is non empty Relation-like the carrier of f2 -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of f2, the carrier of R^1))
g9 is non empty Relation-like the carrier of f2 -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of f2, the carrier of R^1))
dom g9 is non empty Element of K10( the carrier of f2)
f - g9 is Relation-like the carrier of f2 -defined Function-like complex-valued ext-real-valued real-valued set
rng h is non empty V77() V78() V79() Element of K10( the carrier of (Closed-Interval-TSpace ((- (T / 3)),(T / 3))))
K10( the carrier of (Closed-Interval-TSpace ((- (T / 3)),(T / 3)))) is non empty set
E3 is set
dom g9 is non empty set
(dom g9) /\ (dom g9) is set
g9 . E3 is ext-real real V60() Element of REAL
abs (g9 . E3) is ext-real real V60() Element of REAL
(dom g9) /\ (dom g9) is Element of K10( the carrier of f2)
rng g9 is non empty V77() V78() V79() Element of K10( the carrier of R^1)
E3 is set
dom (f - g9) is set
f1 /\ (dom (f - g9)) is set
(f - g9) . E3 is ext-real real V60() Element of REAL
abs ((f - g9) . E3) is ext-real real V60() Element of REAL
dom (f - g9) is Element of K10( the carrier of f2)
f1 /\ (dom (f - g9)) is Element of K10( the carrier of f2)
f . E3 is ext-real real V60() Element of REAL
g9 . E3 is ext-real real V60() Element of REAL
(f . E3) - (g9 . E3) is ext-real real V60() Element of REAL
(dom f) /\ (dom g9) is Element of K10( the carrier of f2)
abs (f . E3) is ext-real real V60() Element of REAL
- T is ext-real real V60() set
E2 . E3 is ext-real real V60() Element of REAL
F . 0 is ext-real real V60() Element of REAL
- ((2 * T) / 3) is ext-real real V60() Element of REAL
(- ((2 * T) / 3)) - (T / 3) is ext-real real V60() Element of REAL
(f . E3) + (T / 3) is ext-real real V60() Element of REAL
(- (T / 3)) + (T / 3) is ext-real real V60() Element of REAL
E2 . E3 is ext-real real V60() Element of REAL
F . 1 is ext-real real V60() Element of REAL
(T / 3) + ((2 * T) / 3) is ext-real real V60() Element of REAL
(f . E3) - (T / 3) is ext-real real V60() Element of REAL
- ((2 * T) / 3) is ext-real real V60() Element of REAL
(- ((2 * T) / 3)) + (T / 3) is ext-real real V60() Element of REAL
rng g9 is non empty V77() V78() V79() Element of K10( the carrier of R^1)
- ((2 * T) / 3) is ext-real real V60() Element of REAL
(- (T / 3)) - (T / 3) is ext-real real V60() Element of REAL
(T / 3) - (- (T / 3)) is ext-real real V60() Element of REAL
{0} is non empty functional V77() V78() V79() V80() V81() V82() set
{1} is non empty V77() V78() V79() V80() V81() V82() set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K11( the carrier of T, the carrier of R^1) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T, the carrier of R^1)) is non empty set
f2 is Element of K10( the carrier of T)
f1 is Element of K10( the carrier of T)
C is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
C .: f2 is V77() V78() V79() Element of K10( the carrier of R^1)
K10( the carrier of R^1) is non empty set
C .: f1 is V77() V78() V79() Element of K10( the carrier of R^1)
right_open_halfline (1 / 2) is V77() V78() V79() open Element of K10(REAL)
K351((1 / 2),+infty) is set
R^1 (right_open_halfline (1 / 2)) is V77() V78() V79() open Element of K10( the carrier of K512())
C " (R^1 (right_open_halfline (1 / 2))) is Element of K10( the carrier of T)
left_open_halfline (1 / 2) is V77() V78() V79() open Element of K10(REAL)
K351(-infty,(1 / 2)) is set
R^1 (left_open_halfline (1 / 2)) is V77() V78() V79() open Element of K10( the carrier of K512())
C " (R^1 (left_open_halfline (1 / 2))) is Element of K10( the carrier of T)
[#] R^1 is non empty non proper V77() V78() V79() closed Element of K10( the carrier of R^1)
dom C is non empty Element of K10( the carrier of T)
g2 is set
C . g2 is ext-real real V60() Element of REAL
g2 is set
C . g2 is ext-real real V60() Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K11( the carrier of T, the carrier of R^1) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T, the carrier of R^1)) is non empty set
K10( the carrier of T) is non empty set
f2 is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of R^1))
f1 is Element of the carrier of T
f2 . f1 is ext-real real V60() Element of the carrier of R^1
D is ext-real real V60() set
K10( the carrier of R^1) is non empty set
C is ext-real real V60() Element of the carrier of RealSpace
Ball (C,D) is V77() V78() V79() Element of K10( the carrier of RealSpace)
K10( the carrier of RealSpace) is non empty set
g1 is V77() V78() V79() Element of K10( the carrier of R^1)
g2 is Element of K10( the carrier of T)
f2 .: g2 is V77() V78() V79() Element of K10( the carrier of R^1)
dom f2 is non empty Element of K10( the carrier of T)
f is Element of the carrier of T
f2 . f is ext-real real V60() Element of the carrier of R^1
(f2 . f) - (f2 . f1) is ext-real real V60() set
abs ((f2 . f) - (f2 . f1)) is ext-real real V60() Element of REAL
h is ext-real real V60() Element of the carrier of RealSpace
dist (h,C) is ext-real real V60() Element of REAL
K10( the carrier of R^1) is non empty set
D is V77() V78() V79() Element of K10( the carrier of R^1)
C is ext-real real V60() Element of the carrier of RealSpace
g1 is ext-real real V60() set
Ball (C,g1) is V77() V78() V79() Element of K10( the carrier of RealSpace)
K10( the carrier of RealSpace) is non empty set
g2 is Element of K10( the carrier of T)
f is Element of K10( the carrier of T)
f2 .: f is V77() V78() V79() Element of K10( the carrier of R^1)
h is set
dom f2 is non empty Element of K10( the carrier of T)
g is set
f2 . g is ext-real real V60() Element of REAL
F is Element of the carrier of T
f2 . F is ext-real real V60() Element of the carrier of R^1
(f2 . F) - (f2 . f1) is ext-real real V60() set
abs ((f2 . F) - (f2 . f1)) is ext-real real V60() Element of REAL
- ((f2 . F) - (f2 . f1)) is ext-real real V60() set
abs (- ((f2 . F) - (f2 . f1))) is ext-real real V60() Element of REAL
(f2 . f1) - (f2 . F) is ext-real real V60() set
abs ((f2 . f1) - (f2 . F)) is ext-real real V60() Element of REAL
c₁₂ is ext-real real V60() Element of the carrier of RealSpace
dist (C,c₁₂) is ext-real real V60() Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
PFuncs ( the carrier of T,REAL) is set
K11(NAT,(PFuncs ( the carrier of T,REAL))) is Relation-like set
K10(K11(NAT,(PFuncs ( the carrier of T,REAL)))) is non empty set
K11( the carrier of T, the carrier of R^1) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T, the carrier of R^1)) is non empty set
f2 is Relation-like NAT -defined PFuncs ( the carrier of T,REAL) -valued Function-like quasi_total Element of K10(K11(NAT,(PFuncs ( the carrier of T,REAL))))
lim (f2, the carrier of T) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
K11( the carrier of T,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T,REAL)) is non empty set
dom (lim (f2, the carrier of T)) is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
D is ext-real real V60() set
D / 3 is ext-real real V60() Element of REAL
g1 is ext-real real V60() Element of REAL
g2 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
f2 . g2 is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
f is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
C is Element of the carrier of T
f . C is ext-real real V60() Element of the carrier of R^1
f1 is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of R^1))
f1 . C is ext-real real V60() Element of the carrier of R^1
(f . C) - (f1 . C) is ext-real real V60() set
abs ((f . C) - (f1 . C)) is ext-real real V60() Element of REAL
h is Element of K10( the carrier of T)
g is Element of K10( the carrier of T)
F is Element of the carrier of T
f . F is ext-real real V60() Element of the carrier of R^1
f1 . F is ext-real real V60() Element of the carrier of R^1
(f . F) - (f1 . F) is ext-real real V60() set
abs ((f . F) - (f1 . F)) is ext-real real V60() Element of REAL
- ((f . F) - (f1 . F)) is ext-real real V60() set
abs (- ((f . F) - (f1 . F))) is ext-real real V60() Element of REAL
- (f . F) is ext-real real V60() set
(- (f . F)) + (f1 . F) is ext-real real V60() set
((f . C) - (f1 . C)) + ((- (f . F)) + (f1 . F)) is ext-real real V60() set
abs (((f . C) - (f1 . C)) + ((- (f . F)) + (f1 . F))) is ext-real real V60() Element of REAL
(abs ((f . C) - (f1 . C))) + (abs (- ((f . F) - (f1 . F)))) is ext-real real V60() Element of REAL
g1 + g1 is ext-real real V60() Element of REAL
2 * g1 is ext-real real V60() Element of REAL
(f . F) - (f . C) is ext-real real V60() set
((f . F) - (f . C)) + (((f . C) - (f1 . C)) + ((- (f . F)) + (f1 . F))) is ext-real real V60() set
abs (((f . F) - (f . C)) + (((f . C) - (f1 . C)) + ((- (f . F)) + (f1 . F)))) is ext-real real V60() Element of REAL
abs ((f . F) - (f . C)) is ext-real real V60() Element of REAL
(abs ((f . F) - (f . C))) + (abs (((f . C) - (f1 . C)) + ((- (f . F)) + (f1 . F)))) is ext-real real V60() Element of REAL
g1 + (2 * g1) is ext-real real V60() Element of REAL
(f1 . F) - (f1 . C) is ext-real real V60() set
abs ((f1 . F) - (f1 . C)) is ext-real real V60() Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K11( the carrier of T, the carrier of R^1) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T, the carrier of R^1)) is non empty set
f2 is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of R^1))
f1 is non empty ext-real positive non negative real V60() set
- f1 is ext-real non positive real V60() set
Closed-Interval-TSpace ((- f1),f1) is non empty strict TopSpace-like V209() SubSpace of R^1
the carrier of (Closed-Interval-TSpace ((- f1),f1)) is non empty V77() V78() V79() set
K11( the carrier of T, the carrier of (Closed-Interval-TSpace ((- f1),f1))) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T, the carrier of (Closed-Interval-TSpace ((- f1),f1)))) is non empty set
dom f2 is non empty Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
C is set
the carrier of T /\ (dom f2) is Element of K10( the carrier of T)
f2 . C is ext-real real V60() Element of REAL
abs (f2 . C) is ext-real real V60() Element of REAL
2 * (abs (f2 . C)) is ext-real real V60() Element of REAL
2 * f1 is ext-real non negative real V60() Element of REAL
abs 2 is ext-real real V60() V66() Element of REAL
(abs 2) * (abs (f2 . C)) is ext-real real V60() Element of REAL
- 2 is ext-real non positive real V60() Element of REAL
abs (- 2) is ext-real real V60() Element of REAL
(abs (- 2)) * (abs (f2 . C)) is ext-real real V60() Element of REAL
(- 2) * (f2 . C) is ext-real real V60() Element of REAL
abs ((- 2) * (f2 . C)) is ext-real real V60() Element of REAL
f1 - (- f1) is non empty ext-real positive non negative real V60() set
(- f1) + f1 is ext-real real V60() set
2 * (f2 . C) is ext-real real V60() Element of REAL
((- f1) + f1) - (2 * (f2 . C)) is ext-real real V60() Element of REAL
abs (((- f1) + f1) - (2 * (f2 . C))) is ext-real real V60() Element of REAL
[.(- f1),f1.] is V77() V78() V79() Element of K10(REAL)
C is set
dom f2 is non empty set
the carrier of T /\ (dom f2) is set
f2 . C is ext-real real V60() Element of REAL
abs (f2 . C) is ext-real real V60() Element of REAL
the carrier of T /\ (dom f2) is Element of K10( the carrier of T)
[.(- f1),f1.] is V77() V78() V79() Element of K10(REAL)
(- f1) + f1 is ext-real real V60() set
2 * (f2 . C) is ext-real real V60() Element of REAL
((- f1) + f1) - (2 * (f2 . C)) is ext-real real V60() Element of REAL
abs (((- f1) + f1) - (2 * (f2 . C))) is ext-real real V60() Element of REAL
f1 - (- f1) is non empty ext-real positive non negative real V60() set
- 2 is ext-real non positive real V60() Element of REAL
(- 2) * (f2 . C) is ext-real real V60() Element of REAL
abs ((- 2) * (f2 . C)) is ext-real real V60() Element of REAL
abs (- 2) is ext-real real V60() Element of REAL
(abs (- 2)) * (abs (f2 . C)) is ext-real real V60() Element of REAL
2 * f1 is ext-real non negative real V60() Element of REAL
abs 2 is ext-real real V60() V66() Element of REAL
(abs 2) * (abs (f2 . C)) is ext-real real V60() Element of REAL
2 * (abs (f2 . C)) is ext-real real V60() Element of REAL
(2 * (abs (f2 . C))) / 2 is ext-real real V60() Element of REAL
(2 * f1) / 2 is ext-real non negative real V60() Element of REAL
T is ext-real real V60() set
f2 is set
f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
C is Relation-like Function-like complex-valued ext-real-valued real-valued set
f1 - C is Relation-like Function-like complex-valued ext-real-valued real-valued set
C - f1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
D is set
dom (C - f1) is set
f2 /\ (dom (C - f1)) is set
(C - f1) . D is ext-real real V60() Element of REAL
abs ((C - f1) . D) is ext-real real V60() Element of REAL
dom (f1 - C) is set
dom f1 is set
dom C is set
(dom f1) /\ (dom C) is set
(f1 - C) . D is ext-real real V60() Element of REAL
abs ((f1 - C) . D) is ext-real real V60() Element of REAL
f1 . D is ext-real real V60() Element of REAL
C . D is ext-real real V60() Element of REAL
(f1 . D) - (C . D) is ext-real real V60() Element of REAL
abs ((f1 . D) - (C . D)) is ext-real real V60() Element of REAL
- ((f1 . D) - (C . D)) is ext-real real V60() Element of REAL
abs (- ((f1 . D) - (C . D))) is ext-real real V60() Element of REAL
(C . D) - (f1 . D) is ext-real real V60() Element of REAL
abs ((C . D) - (f1 . D)) is ext-real real V60() Element of REAL
- 1 is ext-real non positive real V60() Element of REAL
Closed-Interval-TSpace ((- 1),1) is non empty strict TopSpace-like V209() SubSpace of R^1
the carrier of (Closed-Interval-TSpace ((- 1),1)) is non empty V77() V78() V79() set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K11( the carrier of T, the carrier of (Closed-Interval-TSpace ((- 1),1))) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T, the carrier of (Closed-Interval-TSpace ((- 1),1)))) is non empty set
f2 is closed Element of K10( the carrier of T)
T | f2 is strict TopSpace-like closed SubSpace of T
the carrier of (T | f2) is set
K11( the carrier of (T | f2), the carrier of (Closed-Interval-TSpace ((- 1),1))) is Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of (T | f2), the carrier of (Closed-Interval-TSpace ((- 1),1)))) is non empty set
f1 is Relation-like the carrier of (T | f2) -defined the carrier of (Closed-Interval-TSpace ((- 1),1)) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of (T | f2), the carrier of (Closed-Interval-TSpace ((- 1),1))))
[.(- 1),1.] is non empty V77() V78() V79() Element of K10(REAL)
R^1 0 is ext-real real V60() Element of the carrier of K512()
T --> (R^1 0) is non empty Relation-like the carrier of T -defined the carrier of K512() -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of K512()))
K11( the carrier of T, the carrier of K512()) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T, the carrier of K512())) is non empty set
the carrier of T --> (R^1 0) is non empty Relation-like the carrier of T -defined the carrier of K512() -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of K512()))
the carrier of T --> 0 is non empty Relation-like the carrier of T -defined NAT -valued RAT -valued INT -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued natural-valued Function-yielding V231() Element of K10(K11( the carrier of T,NAT))
K11( the carrier of T,NAT) is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K10(K11( the carrier of T,NAT)) is non empty set
rng (T --> (R^1 0)) is non empty V77() V78() V79() Element of K10( the carrier of K512())
g1 is set
g1 is non empty Relation-like the carrier of T -defined the carrier of (Closed-Interval-TSpace ((- 1),1)) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of (Closed-Interval-TSpace ((- 1),1))))
g2 is non empty Relation-like the carrier of T -defined the carrier of (Closed-Interval-TSpace ((- 1),1)) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of (Closed-Interval-TSpace ((- 1),1))))
g2 | f2 is Relation-like the carrier of T -defined f2 -defined the carrier of T -defined the carrier of (Closed-Interval-TSpace ((- 1),1)) -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of (Closed-Interval-TSpace ((- 1),1))))
C is empty proper ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional real V60() complex-valued ext-real-valued real-valued natural-valued V77() V78() V79() V80() V81() V82() V83() closed Function-yielding V231() Element of K10( the carrier of T)
g2 | C is empty proper ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding the carrier of T -defined C -defined the carrier of T -defined RAT -valued the carrier of (Closed-Interval-TSpace ((- 1),1)) -valued Function-like one-to-one constant functional real V60() complex-valued ext-real-valued real-valued natural-valued V77() V78() V79() V80() V81() V82() V83() Function-yielding V231() Element of K10(K11( the carrier of T, the carrier of (Closed-Interval-TSpace ((- 1),1))))
Funcs ( the carrier of T, the carrier of R^1) is non empty functional FUNCTION_DOMAIN of the carrier of T, the carrier of R^1
K11( the carrier of T, the carrier of R^1) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T, the carrier of R^1)) is non empty set
{ b₁ where b₁ is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total Element of Funcs ( the carrier of T, the carrier of R^1) : b₁ is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1)) } is set
C is non empty Element of K10( the carrier of T)
T | C is non empty strict TopSpace-like SubSpace of T
the carrier of (T | C) is non empty set
K11( the carrier of (T | C), the carrier of R^1) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of (T | C), the carrier of R^1)) is non empty set
2 / 3 is ext-real non negative real V60() Element of REAL
1 / 3 is ext-real non negative real V60() Element of REAL
g2 is non empty Relation-like the carrier of (T | C) -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of (T | C), the carrier of R^1))
R^1 0 is ext-real real V60() Element of the carrier of K512()
T --> (R^1 0) is non empty Relation-like the carrier of T -defined the carrier of K512() -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of K512()))
K11( the carrier of T, the carrier of K512()) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T, the carrier of K512())) is non empty set
the carrier of T --> (R^1 0) is non empty Relation-like the carrier of T -defined the carrier of K512() -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of K512()))
f is non empty Relation-like the carrier of (T | C) -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of (T | C), the carrier of R^1))
g is set
dom f is non empty set
f2 /\ (dom f) is set
f . g is ext-real real V60() Element of REAL
abs (f . g) is ext-real real V60() Element of REAL
dom f is non empty Element of K10( the carrier of (T | C))
K10( the carrier of (T | C)) is non empty set
f2 /\ (dom f) is Element of K10( the carrier of (T | C))
rng f is non empty V77() V78() V79() Element of K10( the carrier of R^1)
K10( the carrier of R^1) is non empty set
2 * 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
(2 * 1) / 3 is ext-real non negative real V60() Element of REAL
g is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
dom g is non empty Element of K10( the carrier of T)
f - g is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
h is non empty set
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
(2 / 3) |^ c₁₂ is ext-real real V60() Element of REAL
(2 / 3) * ((2 / 3) |^ c₁₂) is ext-real real V60() Element of REAL
c₁₂ + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
(2 / 3) |^ (c₁₂ + 1) is ext-real real V60() Element of REAL
(1 / 3) * ((2 / 3) |^ (c₁₂ + 1)) is ext-real real V60() Element of REAL
(2 / 3) * ((2 / 3) |^ (c₁₂ + 1)) is ext-real real V60() Element of REAL
F is Element of h
E2 is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total Element of Funcs ( the carrier of T, the carrier of R^1)
g1 is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
f1 - g1 is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
g1 is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
f1 - g1 is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
g1 | f2 is Relation-like the carrier of T -defined f2 -defined the carrier of T -defined the carrier of R^1 -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of R^1))
h is non empty Relation-like the carrier of (T | C) -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of (T | C), the carrier of R^1))
h is non empty Relation-like the carrier of (T | C) -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of (T | C), the carrier of R^1))
f1 - h is Relation-like the carrier of (T | C) -defined Function-like complex-valued ext-real-valued real-valued set
K11( the carrier of (T | C),REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of (T | C),REAL)) is non empty set
f - h is non empty Relation-like the carrier of (T | C) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of (T | C),REAL))
K11( the carrier of T,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T,REAL)) is non empty set
E29 is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
g9 is non empty Relation-like the carrier of (T | C) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of (T | C),REAL))
E3 is non empty Relation-like the carrier of (T | C) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of (T | C),REAL))
g9 - E3 is non empty Relation-like the carrier of (T | C) -defined the carrier of (T | C) -defined REAL -valued Function-like total total quasi_total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of (T | C),REAL))
dom f1 is Element of K10( the carrier of (T | f2))
K10( the carrier of (T | f2)) is non empty set
dom h is non empty Element of K10( the carrier of (T | C))
K10( the carrier of (T | C)) is non empty set
(2 / 3) * 0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional real V60() complex-valued ext-real-valued real-valued natural-valued V77() V78() V79() V80() V81() V82() V83() Function-yielding V231() Element of REAL
((2 / 3) * ((2 / 3) |^ c₁₂)) / 3 is ext-real real V60() Element of REAL
k is non empty Relation-like the carrier of (T | C) -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of (T | C), the carrier of R^1))
2 * ((2 / 3) * ((2 / 3) |^ c₁₂)) is ext-real real V60() Element of REAL
(2 * ((2 / 3) * ((2 / 3) |^ c₁₂))) / 3 is ext-real real V60() Element of REAL
g is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
dom g is non empty Element of K10( the carrier of T)
k - g is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
ga is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
a is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T,REAL))
ga is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T,REAL))
a + ga is non empty Relation-like the carrier of T -defined the carrier of T -defined REAL -valued Function-like total total quasi_total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T,REAL))
y1 is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
y is Element of h
g1 + g is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(f1 - g1) - g is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
(f1 - h) - g is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
((f1 - h) - g) | f2 is Relation-like f2 -defined the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
(f1 - h) | f2 is Relation-like f2 -defined the carrier of (T | C) -defined Function-like complex-valued ext-real-valued real-valued set
((f1 - h) | f2) - g is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
h | f2 is Relation-like f2 -defined the carrier of (T | C) -defined the carrier of R^1 -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of (T | C), the carrier of R^1))
f1 - (h | f2) is Relation-like f2 -defined Function-like complex-valued ext-real-valued real-valued set
(f1 - (h | f2)) - g is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
f1 - (g1 | f2) is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
(f1 - (g1 | f2)) - g is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
(f1 - g1) | f2 is Relation-like f2 -defined the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
((f1 - g1) | f2) - g is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
((f1 - g1) - g) | f2 is Relation-like f2 -defined the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
dom ((f1 - h) - g) is Element of K10( the carrier of T)
dom (f1 - h) is Element of K10( the carrier of (T | C))
(dom (f1 - h)) /\ (dom g) is Element of K10( the carrier of T)
(dom f1) /\ (dom h) is Element of K10( the carrier of (T | C))
((dom f1) /\ (dom h)) /\ (dom g) is Element of K10( the carrier of T)
g1 is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
f1 - g1 is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
K11(NAT,h) is non empty Relation-like set
K10(K11(NAT,h)) is non empty set
F is Element of h
c₁₂ is non empty Relation-like NAT -defined h -valued Function-like total quasi_total Element of K10(K11(NAT,h))
c₁₂ . 0 is Element of h
F is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
c₁₂ . F is Element of h
F + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
c₁₂ . (F + 1) is Element of h
(2 / 3) |^ F is ext-real real V60() Element of REAL
(2 / 3) * ((2 / 3) |^ F) is ext-real real V60() Element of REAL
(2 / 3) |^ (F + 1) is ext-real real V60() Element of REAL
(1 / 3) * ((2 / 3) |^ (F + 1)) is ext-real real V60() Element of REAL
(2 / 3) * ((2 / 3) |^ (F + 1)) is ext-real real V60() Element of REAL
K11( the carrier of T,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T,REAL)) is non empty set
E2 is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
f1 - E2 is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
g1 is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
E2 + g1 is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(f1 - E2) - g1 is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
dom c₁₂ is non empty V77() V78() V79() V80() V81() V82() Element of K10(NAT)
PFuncs ( the carrier of T,REAL) is set
K11(NAT,(PFuncs ( the carrier of T,REAL))) is Relation-like set
K10(K11(NAT,(PFuncs ( the carrier of T,REAL)))) is non empty set
F is Relation-like NAT -defined PFuncs ( the carrier of T,REAL) -valued Function-like quasi_total Element of K10(K11(NAT,(PFuncs ( the carrier of T,REAL))))
F . 0 is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(2 / 3) |^ 0 is ext-real real V60() Element of REAL
(2 / 3) * ((2 / 3) |^ 0) is ext-real real V60() Element of REAL
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
F . (0 + 1) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(2 / 3) |^ (0 + 1) is ext-real real V60() Element of REAL
(1 / 3) * ((2 / 3) |^ (0 + 1)) is ext-real real V60() Element of REAL
(2 / 3) * ((2 / 3) |^ (0 + 1)) is ext-real real V60() Element of REAL
E2 is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
f1 - E2 is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
g1 is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
E2 + g1 is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(f1 - E2) - g1 is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
g1 is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
E2 + g1 is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(f1 - E2) - g1 is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
dom g1 is non empty Element of K10( the carrier of T)
dom E2 is non empty Element of K10( the carrier of T)
9 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
2 / 9 is ext-real non negative real V60() Element of REAL
dom f1 is Element of K10( the carrier of (T | f2))
K10( the carrier of (T | f2)) is non empty set
[#] (T | C) is non empty non proper closed Element of K10( the carrier of (T | C))
K10( the carrier of (T | C)) is non empty set
h is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
F . h is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(2 / 3) |^ h is ext-real real V60() Element of REAL
(2 / 3) * ((2 / 3) |^ h) is ext-real real V60() Element of REAL
h + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
F . (h + 1) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(2 / 3) |^ (h + 1) is ext-real real V60() Element of REAL
(1 / 3) * ((2 / 3) |^ (h + 1)) is ext-real real V60() Element of REAL
(2 / 3) * ((2 / 3) |^ (h + 1)) is ext-real real V60() Element of REAL
h is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
f1 - h is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
h + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
F . (h + 1) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(F . h) - (F . (h + 1)) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(2 / 3) to_power h is ext-real real V60() set
(2 / 9) * ((2 / 3) to_power h) is ext-real real V60() Element of REAL
(F . h) - f1 is Relation-like the carrier of (T | f2) -defined Function-like complex-valued ext-real-valued real-valued set
(2 / 3) * ((2 / 3) to_power h) is ext-real real V60() Element of REAL
z is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
h + z is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(f1 - h) - z is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
z is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
h + z is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(f1 - h) - z is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
dom ((f1 - h) - z) is Element of K10( the carrier of T)
dom (f1 - h) is Element of K10( the carrier of T)
dom z is non empty Element of K10( the carrier of T)
(dom (f1 - h)) /\ (dom z) is Element of K10( the carrier of T)
dom h is non empty Element of K10( the carrier of T)
(dom f1) /\ (dom h) is Element of K10( the carrier of T)
((dom f1) /\ (dom h)) /\ (dom z) is Element of K10( the carrier of T)
(dom f1) /\ the carrier of T is Element of K10( the carrier of (T | f2))
((dom f1) /\ the carrier of T) /\ (dom z) is Element of K10( the carrier of T)
(dom f1) /\ (dom z) is Element of K10( the carrier of T)
(h + 1) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
F . ((h + 1) + 1) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(2 / 3) |^ ((h + 1) + 1) is ext-real real V60() Element of REAL
(1 / 3) * ((2 / 3) |^ ((h + 1) + 1)) is ext-real real V60() Element of REAL
(2 / 3) * ((2 / 3) |^ ((h + 1) + 1)) is ext-real real V60() Element of REAL
E3 is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
f1 - E3 is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
f1 - (h + z) is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
dom (f1 - (h + z)) is Element of K10( the carrier of T)
dom (h + z) is non empty Element of K10( the carrier of T)
(dom f1) /\ (dom (h + z)) is Element of K10( the carrier of T)
(dom h) /\ (dom z) is Element of K10( the carrier of T)
f2 /\ ((dom h) /\ (dom z)) is Element of K10( the carrier of T)
(dom h) /\ the carrier of T is Element of K10( the carrier of T)
f2 /\ ((dom h) /\ the carrier of T) is Element of K10( the carrier of T)
the carrier of T /\ the carrier of T is set
f2 /\ ( the carrier of T /\ the carrier of T) is Element of K10( the carrier of T)
f2 /\ (dom h) is Element of K10( the carrier of T)
f2 /\ the carrier of T is Element of K10( the carrier of T)
gx is set
((f1 - h) - z) . gx is ext-real real V60() Element of REAL
(f1 - h) . gx is ext-real real V60() Element of REAL
z . gx is ext-real real V60() Element of REAL
((f1 - h) . gx) - (z . gx) is ext-real real V60() Element of REAL
f1 . gx is ext-real real V60() Element of REAL
h . gx is ext-real real V60() Element of REAL
(f1 . gx) - (h . gx) is ext-real real V60() Element of REAL
((f1 . gx) - (h . gx)) - (z . gx) is ext-real real V60() Element of REAL
(h . gx) + (z . gx) is ext-real real V60() Element of REAL
(f1 . gx) - ((h . gx) + (z . gx)) is ext-real real V60() Element of REAL
(h + z) . gx is ext-real real V60() Element of REAL
(f1 . gx) - ((h + z) . gx) is ext-real real V60() Element of REAL
(f1 - (h + z)) . gx is ext-real real V60() Element of REAL
gx is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
E3 + gx is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(f1 - E3) - gx is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
gx is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
E3 + gx is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(f1 - E3) - gx is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
dom gx is non empty Element of K10( the carrier of T)
dom E3 is non empty Element of K10( the carrier of T)
(2 / 3) to_power (h + 1) is ext-real real V60() Element of REAL
(2 / 9) * ((2 / 3) to_power (h + 1)) is ext-real real V60() Element of REAL
(1 / 3) * (2 / 3) is ext-real non negative real V60() Element of REAL
((1 / 3) * (2 / 3)) * ((2 / 3) |^ (h + 1)) is ext-real real V60() Element of REAL
(1 / 3) * ((2 / 3) * ((2 / 3) |^ (h + 1))) is ext-real real V60() Element of REAL
gx + E3 is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(gx + E3) - E3 is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
dom ((gx + E3) - E3) is non empty Element of K10( the carrier of T)
dom (gx + E3) is non empty Element of K10( the carrier of T)
(dom (gx + E3)) /\ (dom E3) is Element of K10( the carrier of T)
(dom gx) /\ (dom E3) is Element of K10( the carrier of T)
((dom gx) /\ (dom E3)) /\ (dom E3) is Element of K10( the carrier of T)
a is set
((gx + E3) - E3) . a is ext-real real V60() Element of REAL
(gx + E3) . a is ext-real real V60() Element of REAL
E3 . a is ext-real real V60() Element of REAL
((gx + E3) . a) - (E3 . a) is ext-real real V60() Element of REAL
gx . a is ext-real real V60() Element of REAL
(gx . a) + (E3 . a) is ext-real real V60() Element of REAL
((gx . a) + (E3 . a)) - (E3 . a) is ext-real real V60() Element of REAL
(F . ((h + 1) + 1)) - (F . (h + 1)) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(2 / 3) * ((2 / 3) to_power (h + 1)) is ext-real real V60() Element of REAL
E29 is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T,REAL))
g9 is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T,REAL))
E29 + g9 is non empty Relation-like the carrier of T -defined the carrier of T -defined REAL -valued Function-like total total quasi_total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T,REAL))
f1 - (F . (h + 1)) is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
(h + 1) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
F . ((h + 1) + 1) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(F . (h + 1)) - (F . ((h + 1) + 1)) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(2 / 3) to_power (h + 1) is ext-real real V60() set
(2 / 9) * ((2 / 3) to_power (h + 1)) is ext-real real V60() Element of REAL
(F . (h + 1)) - f1 is Relation-like the carrier of (T | f2) -defined Function-like complex-valued ext-real-valued real-valued set
(2 / 3) * ((2 / 3) to_power (h + 1)) is ext-real real V60() Element of REAL
g1 + E2 is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(g1 + E2) - E2 is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
dom ((g1 + E2) - E2) is non empty Element of K10( the carrier of T)
dom (g1 + E2) is non empty Element of K10( the carrier of T)
(dom (g1 + E2)) /\ (dom E2) is Element of K10( the carrier of T)
(dom g1) /\ (dom E2) is Element of K10( the carrier of T)
((dom g1) /\ (dom E2)) /\ (dom E2) is Element of K10( the carrier of T)
h is set
((g1 + E2) - E2) . h is ext-real real V60() Element of REAL
(g1 + E2) . h is ext-real real V60() Element of REAL
E2 . h is ext-real real V60() Element of REAL
((g1 + E2) . h) - (E2 . h) is ext-real real V60() Element of REAL
g1 . h is ext-real real V60() Element of REAL
(g1 . h) + (E2 . h) is ext-real real V60() Element of REAL
((g1 . h) + (E2 . h)) - (E2 . h) is ext-real real V60() Element of REAL
(F . (0 + 1)) - (F . 0) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(2 / 3) to_power 0 is ext-real real V60() Element of REAL
(2 / 3) |^ 1 is ext-real real V60() Element of REAL
(1 / 3) * ((2 / 3) |^ 1) is ext-real real V60() Element of REAL
(F . 0) - (F . (0 + 1)) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(2 / 3) to_power 0 is ext-real real V60() set
(2 / 9) * ((2 / 3) to_power 0) is ext-real real V60() Element of REAL
(F . 0) - f1 is Relation-like the carrier of (T | f2) -defined Function-like complex-valued ext-real-valued real-valued set
(2 / 3) * ((2 / 3) to_power 0) is ext-real real V60() Element of REAL
h is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() set
F . h is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
h + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
F . (h + 1) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(F . h) - (F . (h + 1)) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(2 / 3) to_power h is ext-real real V60() set
(2 / 9) * ((2 / 3) to_power h) is ext-real real V60() Element of REAL
rng f1 is V77() V78() V79() Element of K10( the carrier of (Closed-Interval-TSpace ((- 1),1)))
K10( the carrier of (Closed-Interval-TSpace ((- 1),1))) is non empty set
K11(C,REAL) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11(C,REAL)) is non empty set
h is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
F . h is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
h + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() V61() V66() V77() V78() V79() V80() V81() V82() Element of NAT
F . (h + 1) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(2 / 3) |^ h is ext-real real V60() Element of REAL
(2 / 3) * ((2 / 3) |^ h) is ext-real real V60() Element of REAL
(2 / 3) |^ (h + 1) is ext-real real V60() Element of REAL
(1 / 3) * ((2 / 3) |^ (h + 1)) is ext-real real V60() Element of REAL
(2 / 3) * ((2 / 3) |^ (h + 1)) is ext-real real V60() Element of REAL
dom (F . h) is Element of K10( the carrier of T)
h is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
f1 - h is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
z is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
h + z is non empty Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(f1 - h) - z is Relation-like the carrier of T -defined Function-like complex-valued ext-real-valued real-valued set
h is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() set
F . h is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
(F . h) - f1 is Relation-like the carrier of (T | f2) -defined Function-like complex-valued ext-real-valued real-valued set
(2 / 3) to_power h is ext-real real V60() set
(2 / 3) * ((2 / 3) to_power h) is ext-real real V60() Element of REAL
lim (F, the carrier of T) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
h is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
h | C is Relation-like the carrier of T -defined C -defined the carrier of T -defined the carrier of R^1 -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of R^1))
lim (F,C) is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T,REAL))
h is set
dom h is non empty set
the carrier of T /\ (dom h) is set
h . h is ext-real real V60() Element of REAL
abs (h . h) is ext-real real V60() Element of REAL
dom h is non empty Element of K10( the carrier of T)
the carrier of T /\ (dom h) is Element of K10( the carrier of T)
dom (F . 0) is Element of K10( the carrier of T)
z is Element of the carrier of T
the carrier of T /\ (dom (F . 0)) is Element of K10( the carrier of T)
(F . 0) . z is ext-real real V60() Element of REAL
|.((F . 0) . z).| is ext-real real V60() Element of REAL
- (1 / 3) is ext-real non positive real V60() Element of REAL
1 - (2 / 3) is ext-real real V60() Element of REAL
(2 / 9) / (1 - (2 / 3)) is ext-real real V60() Element of REAL
(- (1 / 3)) - ((2 / 9) / (1 - (2 / 3))) is ext-real real V60() Element of REAL
((F . 0) . z) - ((2 / 9) / (1 - (2 / 3))) is ext-real real V60() Element of REAL
((F . 0) . z) + ((2 / 9) / (1 - (2 / 3))) is ext-real real V60() Element of REAL
(1 / 3) + ((2 / 9) / (1 - (2 / 3))) is ext-real real V60() Element of REAL
h . z is ext-real real V60() Element of the carrier of R^1
R^1 [.(- 1),1.] is non empty V77() V78() V79() Element of K10( the carrier of K512())
[#] (Closed-Interval-TSpace ((- 1),1)) is non empty non proper V77() V78() V79() closed Element of K10( the carrier of (Closed-Interval-TSpace ((- 1),1)))
R^1 | (R^1 [.(- 1),1.]) is non empty strict TopSpace-like V209() SubSpace of R^1
h is non empty Relation-like the carrier of T -defined the carrier of (Closed-Interval-TSpace ((- 1),1)) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of (Closed-Interval-TSpace ((- 1),1))))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K11( the carrier of T, the carrier of (Closed-Interval-TSpace ((- 1),1))) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T, the carrier of (Closed-Interval-TSpace ((- 1),1)))) is non empty set
K11( the carrier of T, the carrier of R^1) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T, the carrier of R^1)) is non empty set
R^1 1 is ext-real real V60() Element of the carrier of K512()
T --> (R^1 1) is non empty Relation-like the carrier of T -defined the carrier of K512() -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of K512()))
K11( the carrier of T, the carrier of K512()) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of T, the carrier of K512())) is non empty set
the carrier of T --> (R^1 1) is non empty Relation-like the carrier of T -defined the carrier of K512() -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of K512()))
R^1 0 is ext-real real V60() Element of the carrier of K512()
T --> (R^1 0) is non empty Relation-like the carrier of T -defined the carrier of K512() -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of K512()))
the carrier of T --> (R^1 0) is non empty Relation-like the carrier of T -defined the carrier of K512() -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of K512()))
C is non empty closed Element of K10( the carrier of T)
D is non empty closed Element of K10( the carrier of T)
T | C is non empty strict TopSpace-like closed SubSpace of T
(T --> (R^1 0)) | (T | C) is non empty Relation-like the carrier of (T | C) -defined the carrier of K512() -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of (T | C), the carrier of K512()))
the carrier of (T | C) is non empty set
K11( the carrier of (T | C), the carrier of K512()) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of (T | C), the carrier of K512())) is non empty set
T | D is non empty strict TopSpace-like closed SubSpace of T
(T --> (R^1 1)) | (T | D) is non empty Relation-like the carrier of (T | D) -defined the carrier of K512() -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of (T | D), the carrier of K512()))
the carrier of (T | D) is non empty set
K11( the carrier of (T | D), the carrier of K512()) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of (T | D), the carrier of K512())) is non empty set
((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D)) is non empty Relation-like the carrier of ((T | C) union (T | D)) -defined the carrier of K512() -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of ((T | C) union (T | D)), the carrier of K512()))
(T | C) union (T | D) is non empty strict TopSpace-like SubSpace of T
the carrier of ((T | C) union (T | D)) is non empty set
K11( the carrier of ((T | C) union (T | D)), the carrier of K512()) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of ((T | C) union (T | D)), the carrier of K512())) is non empty set
(T --> (R^1 1)) | the carrier of (T | D) is Relation-like the carrier of T -defined the carrier of (T | D) -defined the carrier of T -defined the carrier of K512() -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of K512()))
rng ((T --> (R^1 1)) | (T | D)) is non empty V77() V78() V79() Element of K10( the carrier of K512())
rng (T --> (R^1 1)) is non empty V77() V78() V79() Element of K10( the carrier of K512())
(T --> (R^1 0)) | the carrier of (T | C) is Relation-like the carrier of T -defined the carrier of (T | C) -defined the carrier of T -defined the carrier of K512() -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of K512()))
rng ((T --> (R^1 0)) | (T | C)) is non empty V77() V78() V79() Element of K10( the carrier of K512())
rng (T --> (R^1 0)) is non empty V77() V78() V79() Element of K10( the carrier of K512())
(rng ((T --> (R^1 0)) | (T | C))) \/ (rng ((T --> (R^1 1)) | (T | D))) is non empty V77() V78() V79() Element of K10( the carrier of K512())
(rng (T --> (R^1 0))) \/ (rng (T --> (R^1 1))) is non empty V77() V78() V79() Element of K10( the carrier of K512())
the carrier of T --> 0 is non empty Relation-like the carrier of T -defined NAT -valued RAT -valued INT -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued natural-valued Function-yielding V231() Element of K10(K11( the carrier of T,NAT))
K11( the carrier of T,NAT) is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K10(K11( the carrier of T,NAT)) is non empty set
the carrier of T --> 1 is non empty Relation-like non-empty the carrier of T -defined NAT -valued RAT -valued INT -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K10(K11( the carrier of T,NAT))
rng (((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) is non empty V77() V78() V79() Element of K10( the carrier of K512())
[.(- 1),1.] is non empty V77() V78() V79() Element of K10(REAL)
h is set
C \/ D is non empty Element of K10( the carrier of T)
T | (C \/ D) is non empty strict TopSpace-like SubSpace of T
the carrier of (T | (C \/ D)) is non empty set
(T --> (R^1 1)) .: D is V77() V78() V79() Element of K10( the carrier of K512())
h is set
g is set
dom (T --> (R^1 1)) is non empty Element of K10( the carrier of T)
(T --> (R^1 1)) . g is ext-real real V60() Element of REAL
(T --> (R^1 0)) .: C is V77() V78() V79() Element of K10( the carrier of K512())
h is set
g is set
dom (T --> (R^1 0)) is non empty Element of K10( the carrier of T)
(T --> (R^1 0)) . g is ext-real real V60() Element of REAL
K11( the carrier of (T | (C \/ D)), the carrier of (Closed-Interval-TSpace ((- 1),1))) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of (T | (C \/ D)), the carrier of (Closed-Interval-TSpace ((- 1),1)))) is non empty set
K11( the carrier of ((T | C) union (T | D)), the carrier of R^1) is non empty Relation-like complex-valued ext-real-valued real-valued set
K10(K11( the carrier of ((T | C) union (T | D)), the carrier of R^1)) is non empty set
h is non empty Relation-like the carrier of (T | (C \/ D)) -defined the carrier of (Closed-Interval-TSpace ((- 1),1)) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of (T | (C \/ D)), the carrier of (Closed-Interval-TSpace ((- 1),1))))
g is non empty Relation-like the carrier of T -defined the carrier of (Closed-Interval-TSpace ((- 1),1)) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of (Closed-Interval-TSpace ((- 1),1))))
g | (C \/ D) is Relation-like the carrier of T -defined C \/ D -defined the carrier of T -defined the carrier of (Closed-Interval-TSpace ((- 1),1)) -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of (Closed-Interval-TSpace ((- 1),1))))
F is non empty Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like total quasi_total complex-valued ext-real-valued real-valued continuous Element of K10(K11( the carrier of T, the carrier of R^1))
F .: C is V77() V78() V79() Element of K10( the carrier of R^1)
K10( the carrier of R^1) is non empty set
F .: D is V77() V78() V79() Element of K10( the carrier of R^1)
(((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) .: C is V77() V78() V79() Element of K10( the carrier of K512())
((T --> (R^1 0)) | (T | C)) .: C is V77() V78() V79() Element of K10( the carrier of K512())
(T --> (R^1 0)) | C is Relation-like the carrier of T -defined C -defined the carrier of T -defined the carrier of K512() -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of K512()))
((T --> (R^1 0)) | C) .: C is V77() V78() V79() Element of K10( the carrier of K512())
(((T --> (R^1 0)) | (T | C)) union ((T --> (R^1 1)) | (T | D))) .: D is V77() V78() V79() Element of K10( the carrier of K512())
((T --> (R^1 1)) | (T | D)) .: D is V77() V78() V79() Element of K10( the carrier of K512())
(T --> (R^1 1)) | D is Relation-like the carrier of T -defined D -defined the carrier of T -defined the carrier of K512() -valued Function-like complex-valued ext-real-valued real-valued Element of K10(K11( the carrier of T, the carrier of K512()))
((T --> (R^1 1)) | D) .: D is V77() V78() V79() Element of K10( the carrier of K512())