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

(f1 . F) . c

f . c

((f1 . F) . c

abs (((f1 . F) . c

f1 # c

(f1 # c

|.(((f1 . F) . c

(f . c

|.((f . c

F is ext-real epsilon-transitive epsilon-connected ordinal natural real V60() set

(f1 # c

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

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

(f1 . (F + 1)) . c

((f1 . F) . c

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

((f1 # c

|.(((f1 # c

lim (f1 # c

(lim (f1 # c

|.((lim (f1 # c

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

f1 # c

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

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

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

(f1 . F) . c

((f1 . F) - (f1 . (F + 1))) . c

((f1 # c

|.(((f1 # c

lim (f1 # c

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

(lim (f1 # c

|.((lim (f1 # c

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

((lim (f1,f2)) . c

|.(((lim (f1,f2)) . c

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

((lim (f1,f2)) . c

|.(((lim (f1,f2)) . c

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

f1 . c

dom (f1 . c

(dom (f1 . c

(f1 . c

dom ((f1 . c

((f1 . c

(f1 . c

g1 . f is ext-real real V60() Element of REAL

((f1 . c

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

D to_power F is ext-real real V60() set

C * (D to_power c

C * (D to_power F) is ext-real real V60() set

(C * (D to_power c

(C * (D to_power c

(C * (D to_power c

(C * (D to_power c

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

|.(((f1 . c

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

abs (((f1 . c

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

(f1 # f) . c

((f1 # f) . c

abs (((f1 # f) . c

f1 . c

(f1 . c

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

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