:: TOPALG_6 semantic presentation

REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V171() non bounded_below non bounded_above interval set

NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V171() bounded_below Element of bool REAL

bool REAL is set

I[01] is non empty strict TopSpace-like T_0 T_1 T_2 real-membered pathwise_connected compact SubSpace of R^1

R^1 is non empty strict TopSpace-like T_0 T_1 T_2 real-membered TopStruct

the carrier of I[01] is non empty complex-membered ext-real-membered real-membered set

[:I[01],I[01]:] is non empty strict TopSpace-like T_0 T_1 T_2 compact TopStruct

the carrier of [:I[01],I[01]:] is non empty set

omega is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V171() bounded_below set

bool omega is set

{} is empty trivial Relation-like non-empty empty-yielding NAT -defined {} -valued Function-like one-to-one constant functional finite finite-yielding V29() onto FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V171() bounded_below bounded_above real-bounded interval Function-yielding V204() set

RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V171() set

the empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V29() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V171() bounded_below bounded_above real-bounded interval Function-yielding V204() set is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V29() FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V171() bounded_below bounded_above real-bounded interval Function-yielding V204() set

1 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

{{},1} is non empty finite set

I[01] is non empty strict TopSpace-like T_0 T_1 T_2 real-membered pathwise_connected compact TopStruct

the carrier of I[01] is non empty complex-membered ext-real-membered real-membered set

INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V171() set

[:1,1:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set

bool [:1,1:] is set

[:[:1,1:],1:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set

bool [:[:1,1:],1:] is set

[:[:1,1:],REAL:] is Relation-like complex-yielding ext-real-valued real-valued set

bool [:[:1,1:],REAL:] is set

[:REAL,REAL:] is Relation-like complex-yielding ext-real-valued real-valued set

[:[:REAL,REAL:],REAL:] is Relation-like complex-yielding ext-real-valued real-valued set

bool [:[:REAL,REAL:],REAL:] is set

2 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

[:2,2:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set

[:[:2,2:],REAL:] is Relation-like complex-yielding ext-real-valued real-valued set

bool [:[:2,2:],REAL:] is set

RealSpace is strict real-membered MetrStruct

[: the carrier of I[01], the carrier of I[01]:] is Relation-like complex-yielding ext-real-valued real-valued set

bool [: the carrier of I[01], the carrier of I[01]:] is set

bool the carrier of [:I[01],I[01]:] is set

bool NAT is set

COMPLEX is non empty non trivial non finite complex-membered V171() set

bool [:REAL,REAL:] is set

TOP-REAL 2 is non empty TopSpace-like V114() V142() V143() V144() V145() V146() V147() V148() strict V243() V244() 2 -locally_euclidean V359() RLTopStruct

the carrier of (TOP-REAL 2) is non empty set

[:I[01],I[01]:] is non empty strict TopSpace-like T_0 T_1 T_2 compact TopStruct

the carrier of [:I[01],I[01]:] is non empty set

[:COMPLEX,COMPLEX:] is Relation-like complex-yielding set

bool [:COMPLEX,COMPLEX:] is set

[:COMPLEX,REAL:] is Relation-like complex-yielding ext-real-valued real-valued set

bool [:COMPLEX,REAL:] is set

R^1 is non empty strict TopSpace-like T_0 T_1 T_2 real-membered pathwise_connected interval SubSpace of R^1

the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set

bool the carrier of R^1 is set

bool (bool the carrier of R^1) is set

Tunit_circle 2 is non empty TopSpace-like pathwise_connected V202() compact SubSpace of TOP-REAL 2

the carrier of (Tunit_circle 2) is non empty set

[: the carrier of R^1, the carrier of (Tunit_circle 2):] is Relation-like set

bool [: the carrier of R^1, the carrier of (Tunit_circle 2):] is set

CircleMap is non empty Relation-like the carrier of R^1 -defined the carrier of R^1 -defined the carrier of (Tunit_circle 2) -valued the carrier of (Tunit_circle 2) -valued Function-like total total quasi_total quasi_total onto continuous Element of bool [: the carrier of R^1, the carrier of (Tunit_circle 2):]

c[10] is Element of the carrier of (Tunit_circle 2)

Topen_unit_circle c[10] is non empty strict TopSpace-like SubSpace of Tunit_circle 2

the carrier of (Topen_unit_circle c[10]) is non empty set

0 is empty trivial ordinal natural real Relation-like non-empty empty-yielding NAT -defined {} -valued Function-like one-to-one constant functional finite finite-yielding V29() onto V101() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V153() V154() complex-yielding ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V171() bounded_below bounded_above real-bounded interval Function-yielding V204() Element of NAT

].0,1.[ is non empty complex-membered ext-real-membered real-membered non left_end non right_end bounded_below bounded_above real-bounded interval Element of bool REAL

R^1 ].0,1.[ is non empty complex-membered ext-real-membered real-membered interval Element of bool the carrier of R^1

R^1 | (R^1 ].0,1.[) is non empty strict TopSpace-like real-membered pathwise_connected interval SubSpace of R^1

the carrier of (R^1 | (R^1 ].0,1.[)) is non empty complex-membered ext-real-membered real-membered set

[: the carrier of (Topen_unit_circle c[10]), the carrier of (R^1 | (R^1 ].0,1.[)):] is Relation-like complex-yielding ext-real-valued real-valued set

bool [: the carrier of (Topen_unit_circle c[10]), the carrier of (R^1 | (R^1 ].0,1.[)):] is set

c[-10] is Element of the carrier of (Tunit_circle 2)

Topen_unit_circle c[-10] is non empty strict TopSpace-like SubSpace of Tunit_circle 2

the carrier of (Topen_unit_circle c[-10]) is non empty set

1 / 2 is real V101() ext-real non negative Element of REAL

3 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

3 / 2 is real V101() ext-real non negative Element of REAL

].(1 / 2),(3 / 2).[ is non empty complex-membered ext-real-membered real-membered non left_end non right_end bounded_below bounded_above real-bounded interval Element of bool REAL

R^1 ].(1 / 2),(3 / 2).[ is non empty complex-membered ext-real-membered real-membered interval Element of bool the carrier of R^1

R^1 | (R^1 ].(1 / 2),(3 / 2).[) is non empty strict TopSpace-like real-membered pathwise_connected interval SubSpace of R^1

the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)) is non empty complex-membered ext-real-membered real-membered set

[: the carrier of (Topen_unit_circle c[-10]), the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)):] is Relation-like complex-yielding ext-real-valued real-valued set

bool [: the carrier of (Topen_unit_circle c[-10]), the carrier of (R^1 | (R^1 ].(1 / 2),(3 / 2).[)):] is set

the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like complex-yielding set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set

[:RAT,RAT:] is Relation-like RAT -valued complex-yielding ext-real-valued real-valued set

bool [:RAT,RAT:] is set

[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued complex-yielding ext-real-valued real-valued set

bool [:[:RAT,RAT:],RAT:] is set

[:INT,INT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued set

bool [:INT,INT:] is set

[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued set

bool [:[:INT,INT:],INT:] is set

[:NAT,NAT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set

[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued complex-yielding ext-real-valued real-valued natural-valued set

bool [:[:NAT,NAT:],NAT:] is set

K687() is non empty V116() L10()

the carrier of K687() is non empty set

K692() is non empty V116() V223() V224() V225() V227() V253() V254() V255() V256() V257() V258() L10()

K693() is non empty V116() V225() V227() V256() V257() V258() M30(K692())

K694() is non empty V116() V223() V225() V227() V256() V257() V258() V259() M33(K692(),K693())

K696() is non empty V116() V223() V225() V227() L10()

K697() is non empty V116() V223() V225() V227() V259() M30(K696())

Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like real-membered SubSpace of R^1

the carrier of (Closed-Interval-TSpace (0,1)) is non empty complex-membered ext-real-membered real-membered set

bool the carrier of (TOP-REAL 2) is set

K743(0,1) is real V101() ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

K744(0,1) is real V101() ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

bool the carrier of R^1 is set

[.0,1.] is complex-membered ext-real-membered real-membered interval Element of bool REAL

0[01] is real V101() ext-real Element of the carrier of I[01]

1[01] is real V101() ext-real Element of the carrier of I[01]

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

5 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

bool the carrier of I[01] is set

Seg 1 is non empty finite V32(1) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

K745(0,1,K743(0,1),K744(0,1)) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):]

[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):] is Relation-like complex-yielding ext-real-valued real-valued set

bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):] is set

id (Closed-Interval-TSpace (0,1)) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like one-to-one total quasi_total onto bijective continuous V100( Closed-Interval-TSpace (0,1), Closed-Interval-TSpace (0,1)) complex-yielding ext-real-valued real-valued being_homeomorphism Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):]

id the carrier of (Closed-Interval-TSpace (0,1)) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like one-to-one total quasi_total onto bijective V70() V72() V73() V77() complex-yielding ext-real-valued real-valued increasing non-decreasing Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):]

K746(0,1,K743(0,1),K744(0,1)) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):]

n is TopSpace-like TopStruct

the carrier of n is set

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

[: the carrier of n, the carrier of r:] is Relation-like set

bool [: the carrier of n, the carrier of r:] is set

x is Relation-like the carrier of n -defined the carrier of r -valued Function-like total quasi_total Element of bool [: the carrier of n, the carrier of r:]

bool the carrier of r is set

f is Element of bool the carrier of r

x " f is Element of bool the carrier of n

bool the carrier of n is set

rng x is Element of bool the carrier of r

bool the carrier of r is set

f is Element of the carrier of r

{f} is non empty trivial finite set

dom x is Element of bool the carrier of n

bool the carrier of n is set

the_value_of x is set

g is set

x . g is set

{(the_value_of x)} is non empty trivial finite set

(dom x) --> (the_value_of x) is Relation-like dom x -defined {(the_value_of x)} -valued Function-like constant total quasi_total Element of bool [:(dom x),{(the_value_of x)}:]

[:(dom x),{(the_value_of x)}:] is Relation-like set

bool [:(dom x),{(the_value_of x)}:] is set

n --> f is Relation-like the carrier of n -defined the carrier of r -valued Function-like total quasi_total continuous Element of bool [: the carrier of n, the carrier of r:]

the carrier of n --> f is Relation-like the carrier of n -defined the carrier of r -valued Function-like constant total quasi_total Element of bool [: the carrier of n, the carrier of r:]

L[01] (0,1,0,1) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):]

(id (Closed-Interval-TSpace (0,1))) * (id (Closed-Interval-TSpace (0,1))) is non empty Relation-like the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -defined the carrier of (Closed-Interval-TSpace (0,1)) -valued the carrier of (Closed-Interval-TSpace (0,1)) -valued Function-like one-to-one total total quasi_total quasi_total onto bijective continuous complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (0,1)):]

r is real V101() ext-real set

n is real V101() ext-real set

x is real V101() ext-real set

f is real V101() ext-real set

C is real V101() ext-real set

g is real V101() ext-real set

Closed-Interval-TSpace (g,C) is non empty strict TopSpace-like real-membered SubSpace of R^1

the carrier of (Closed-Interval-TSpace (g,C)) is non empty complex-membered ext-real-membered real-membered set

Closed-Interval-TSpace (x,f) is non empty strict TopSpace-like real-membered SubSpace of R^1

the carrier of (Closed-Interval-TSpace (x,f)) is non empty complex-membered ext-real-membered real-membered set

Closed-Interval-TSpace (n,r) is non empty strict TopSpace-like real-membered SubSpace of R^1

the carrier of (Closed-Interval-TSpace (n,r)) is non empty complex-membered ext-real-membered real-membered set

L[01] (g,C,n,r) is non empty Relation-like the carrier of (Closed-Interval-TSpace (g,C)) -defined the carrier of (Closed-Interval-TSpace (n,r)) -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (g,C)), the carrier of (Closed-Interval-TSpace (n,r)):]

[: the carrier of (Closed-Interval-TSpace (g,C)), the carrier of (Closed-Interval-TSpace (n,r)):] is Relation-like complex-yielding ext-real-valued real-valued set

bool [: the carrier of (Closed-Interval-TSpace (g,C)), the carrier of (Closed-Interval-TSpace (n,r)):] is set

L[01] (n,r,x,f) is non empty Relation-like the carrier of (Closed-Interval-TSpace (n,r)) -defined the carrier of (Closed-Interval-TSpace (x,f)) -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (n,r)), the carrier of (Closed-Interval-TSpace (x,f)):]

[: the carrier of (Closed-Interval-TSpace (n,r)), the carrier of (Closed-Interval-TSpace (x,f)):] is Relation-like complex-yielding ext-real-valued real-valued set

bool [: the carrier of (Closed-Interval-TSpace (n,r)), the carrier of (Closed-Interval-TSpace (x,f)):] is set

(L[01] (n,r,x,f)) * (L[01] (g,C,n,r)) is non empty Relation-like the carrier of (Closed-Interval-TSpace (g,C)) -defined the carrier of (Closed-Interval-TSpace (x,f)) -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (g,C)), the carrier of (Closed-Interval-TSpace (x,f)):]

[: the carrier of (Closed-Interval-TSpace (g,C)), the carrier of (Closed-Interval-TSpace (x,f)):] is Relation-like complex-yielding ext-real-valued real-valued set

bool [: the carrier of (Closed-Interval-TSpace (g,C)), the carrier of (Closed-Interval-TSpace (x,f)):] is set

L[01] (g,C,x,f) is non empty Relation-like the carrier of (Closed-Interval-TSpace (g,C)) -defined the carrier of (Closed-Interval-TSpace (x,f)) -valued Function-like total quasi_total complex-yielding ext-real-valued real-valued Element of bool [: the carrier of (Closed-Interval-TSpace (g,C)), the carrier of (Closed-Interval-TSpace (x,f)):]

dom ((L[01] (n,r,x,f)) * (L[01] (g,C,n,r))) is non empty complex-membered ext-real-membered real-membered Element of bool the carrier of (Closed-Interval-TSpace (g,C))

bool the carrier of (Closed-Interval-TSpace (g,C)) is set

[#] (Closed-Interval-TSpace (g,C)) is non empty non proper closed complex-membered ext-real-membered real-membered Element of bool the carrier of (Closed-Interval-TSpace (g,C))

dom (L[01] (g,C,x,f)) is non empty complex-membered ext-real-membered real-membered Element of bool the carrier of (Closed-Interval-TSpace (g,C))

U is set

((L[01] (n,r,x,f)) * (L[01] (g,C,n,r))) . U is real V101() ext-real set

(L[01] (g,C,x,f)) . U is real V101() ext-real set

[.g,C.] is complex-membered ext-real-membered real-membered interval Element of bool REAL

V is real V101() ext-real set

rng (L[01] (g,C,n,r)) is non empty complex-membered ext-real-membered real-membered Element of bool REAL

[#] (Closed-Interval-TSpace (n,r)) is non empty non proper closed complex-membered ext-real-membered real-membered Element of bool the carrier of (Closed-Interval-TSpace (n,r))

bool the carrier of (Closed-Interval-TSpace (n,r)) is set

(L[01] (g,C,n,r)) . U is real V101() ext-real set

dom (L[01] (g,C,n,r)) is non empty complex-membered ext-real-membered real-membered Element of bool the carrier of (Closed-Interval-TSpace (g,C))

c is real V101() ext-real set

[.n,r.] is complex-membered ext-real-membered real-membered interval Element of bool REAL

(L[01] (n,r,x,f)) . c is real V101() ext-real set

f - x is real V101() ext-real set

r - n is real V101() ext-real set

(f - x) / (r - n) is real V101() ext-real set

c - n is real V101() ext-real set

((f - x) / (r - n)) * (c - n) is real V101() ext-real set

(((f - x) / (r - n)) * (c - n)) + x is real V101() ext-real set

((f - x) / (r - n)) * c is real V101() ext-real set

C - g is real V101() ext-real set

(r - n) / (C - g) is real V101() ext-real set

V - g is real V101() ext-real set

((r - n) / (C - g)) * (V - g) is real V101() ext-real set

(((r - n) / (C - g)) * (V - g)) + n is real V101() ext-real set

((f - x) / (r - n)) * ((((r - n) / (C - g)) * (V - g)) + n) is real V101() ext-real set

((f - x) / (r - n)) * ((r - n) / (C - g)) is real V101() ext-real set

(((f - x) / (r - n)) * ((r - n) / (C - g))) * (V - g) is real V101() ext-real set

((f - x) / (r - n)) * n is real V101() ext-real set

((((f - x) / (r - n)) * ((r - n) / (C - g))) * (V - g)) + (((f - x) / (r - n)) * n) is real V101() ext-real set

(f - x) / (C - g) is real V101() ext-real set

(r - n) / (r - n) is real V101() ext-real set

((f - x) / (C - g)) * ((r - n) / (r - n)) is real V101() ext-real set

(((f - x) / (C - g)) * ((r - n) / (r - n))) * (V - g) is real V101() ext-real set

((((f - x) / (C - g)) * ((r - n) / (r - n))) * (V - g)) + (((f - x) / (r - n)) * n) is real V101() ext-real set

((f - x) / (C - g)) * 1 is real V101() ext-real set

(((f - x) / (C - g)) * 1) * (V - g) is real V101() ext-real set

((((f - x) / (C - g)) * 1) * (V - g)) + (((f - x) / (r - n)) * n) is real V101() ext-real set

((f - x) / (C - g)) * (V - g) is real V101() ext-real set

(((f - x) / (C - g)) * (V - g)) + (((f - x) / (r - n)) * n) is real V101() ext-real set

(L[01] (n,r,x,f)) . ((L[01] (g,C,n,r)) . U) is real V101() ext-real set

n is non empty ordinal natural real V101() ext-real positive non negative set

TOP-REAL n is non empty TopSpace-like V114() V142() V143() V144() V145() V146() V147() V148() strict V243() V244() n -locally_euclidean V359() RLTopStruct

the carrier of (TOP-REAL n) is non empty set

REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

r is Relation-like Function-like set

dom r is set

r .: (n -tuples_on REAL) is set

x is set

n + 1 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

0 + 1 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

Seg n is non empty finite V32(n) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

f is set

r . f is set

g is Relation-like NAT -defined REAL -valued Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of n -tuples_on REAL

g . 1 is real V101() ext-real set

Funcs ((Seg n),REAL) is non empty functional FUNCTION_DOMAIN of Seg n, REAL

rng g is finite complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded Element of bool REAL

C is Relation-like Function-like set

dom C is set

rng C is set

{x} is non empty trivial finite set

(Seg n) --> x is non empty Relation-like Seg n -defined Seg n -defined {x} -valued Function-like constant finite total total quasi_total FinSequence-like FinSubsequence-like Element of bool [:(Seg n),{x}:]

[:(Seg n),{x}:] is Relation-like finite set

bool [:(Seg n),{x}:] is finite V29() set

dom ((Seg n) --> x) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

rng ((Seg n) --> x) is non empty trivial finite Element of bool {x}

bool {x} is finite V29() set

g is Relation-like NAT -defined REAL -valued Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of n -tuples_on REAL

r . g is set

g . 1 is real V101() ext-real set

r is non empty TopSpace-like TopStruct

the carrier of r is non empty set

x is set

f is Element of the carrier of r

[#] (TOP-REAL n) is non empty non proper closed Element of bool the carrier of (TOP-REAL n)

the carrier of (TOP-REAL n) is non empty non trivial non finite set

bool the carrier of (TOP-REAL n) is set

g is non empty a_neighborhood of f

r | g is non empty strict TopSpace-like SubSpace of r

(TOP-REAL n) | ([#] (TOP-REAL n)) is non empty strict TopSpace-like SubSpace of TOP-REAL n

the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n))) is non empty set

the carrier of (r | g) is non empty set

[: the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n))), the carrier of (r | g):] is Relation-like set

bool [: the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n))), the carrier of (r | g):] is set

C is non empty Relation-like the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n))) -defined the carrier of (r | g) -valued Function-like total quasi_total Element of bool [: the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n))), the carrier of (r | g):]

dom C is non empty Element of bool the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n)))

bool the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n))) is set

[#] ((TOP-REAL n) | ([#] (TOP-REAL n))) is non empty non proper closed Element of bool the carrier of ((TOP-REAL n) | ([#] (TOP-REAL n)))

rng C is non empty Element of bool the carrier of (r | g)

bool the carrier of (r | g) is set

[#] (r | g) is non empty non proper closed Element of bool the carrier of (r | g)

n is ordinal natural real V101() ext-real non negative set

TOP-REAL n is non empty TopSpace-like V114() V142() V143() V144() V145() V146() V147() V148() strict V243() V244() n -locally_euclidean V359() RLTopStruct

the carrier of (TOP-REAL n) is non empty set

0. (TOP-REAL n) is Relation-like NAT -defined Function-like finite V32(n) V45( TOP-REAL n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

the ZeroF of (TOP-REAL n) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

Sphere ((0. (TOP-REAL n)),1) is closed Element of bool the carrier of (TOP-REAL n)

bool the carrier of (TOP-REAL n) is set

r is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

- r is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

- r is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

{r} is non empty trivial functional finite V29() set

(Sphere ((0. (TOP-REAL n)),1)) \ {r} is Element of bool the carrier of (TOP-REAL n)

x is ordinal natural real V101() ext-real non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT

TOP-REAL x is non empty TopSpace-like V114() V142() V143() V144() V145() V146() V147() V148() strict V243() V244() x -locally_euclidean V359() RLTopStruct

the carrier of (TOP-REAL x) is non empty set

f is Relation-like NAT -defined Function-like finite V32(x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)

0. (TOP-REAL x) is Relation-like NAT -defined Function-like finite V32(x) V45( TOP-REAL x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)

the ZeroF of (TOP-REAL x) is Relation-like NAT -defined Function-like finite V32(x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)

f - (0. (TOP-REAL x)) is Relation-like NAT -defined Function-like finite V32(x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)

f - (0. (TOP-REAL x)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

|.(f - (0. (TOP-REAL x))).| is real V101() ext-real non negative Element of REAL

- (0. (TOP-REAL x)) is Relation-like NAT -defined Function-like finite V32(x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)

- (0. (TOP-REAL x)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

f + (- (0. (TOP-REAL x))) is Relation-like NAT -defined Function-like finite V32(x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)

f + (- (0. (TOP-REAL x))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

|.(f + (- (0. (TOP-REAL x)))).| is real V101() ext-real non negative Element of REAL

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

(- 1) * (0. (TOP-REAL n)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(- 1) * (0. (TOP-REAL n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

r + ((- 1) * (0. (TOP-REAL n))) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

r + ((- 1) * (0. (TOP-REAL n))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

|.(r + ((- 1) * (0. (TOP-REAL n)))).| is real V101() ext-real non negative Element of REAL

r + (0. (TOP-REAL n)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

r + (0. (TOP-REAL n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

|.(r + (0. (TOP-REAL n))).| is real V101() ext-real non negative Element of REAL

|.r.| is real V101() ext-real non negative Element of REAL

|.(0. (TOP-REAL n)).| is real V101() ext-real non negative Element of REAL

1 + 1 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

(1 + 1) * r is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(1 + 1) * r is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

g is real V101() ext-real set

g * r is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

g * r is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(g * r) + (g * r) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(g * r) + (g * r) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(g * r) + r is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(g * r) + r is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

r + r is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

r + r is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

r + (- r) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

r + (- r) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

|.(- r).| is real V101() ext-real non negative Element of REAL

(- r) + (0. (TOP-REAL n)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(- r) + (0. (TOP-REAL n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

|.((- r) + (0. (TOP-REAL n))).| is real V101() ext-real non negative Element of REAL

(- r) + ((- 1) * (0. (TOP-REAL n))) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(- r) + ((- 1) * (0. (TOP-REAL n))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

|.((- r) + ((- 1) * (0. (TOP-REAL n)))).| is real V101() ext-real non negative Element of REAL

- (0. (TOP-REAL n)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

- (0. (TOP-REAL n)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(- r) + (- (0. (TOP-REAL n))) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(- r) + (- (0. (TOP-REAL n))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

|.((- r) + (- (0. (TOP-REAL n)))).| is real V101() ext-real non negative Element of REAL

- f is Relation-like NAT -defined Function-like finite V32(x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)

- f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(- f) - (0. (TOP-REAL x)) is Relation-like NAT -defined Function-like finite V32(x) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL x)

(- f) - (0. (TOP-REAL x)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

|.((- f) - (0. (TOP-REAL x))).| is real V101() ext-real non negative Element of REAL

Sphere ((0. (TOP-REAL x)),1) is closed bounded Element of bool the carrier of (TOP-REAL x)

bool the carrier of (TOP-REAL x) is set

n is non empty TopStruct

the carrier of n is non empty set

r is Element of the carrier of n

x is Element of the carrier of n

f is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total Path of r,x

dom f is non empty complex-membered ext-real-membered real-membered Element of bool the carrier of I[01]

bool the carrier of I[01] is set

inf (dom f) is ext-real set

sup (dom f) is ext-real set

n is non empty TopSpace-like TopStruct

the carrier of n is non empty set

r is Element of the carrier of n

x is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like constant total quasi_total continuous Path of r,r

f is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like constant total quasi_total continuous Path of r,r

I[01] --> r is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of n:]

[: the carrier of I[01], the carrier of n:] is Relation-like set

bool [: the carrier of I[01], the carrier of n:] is set

the carrier of I[01] --> r is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like constant total quasi_total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of n:]

n is non empty TopSpace-like TopStruct

the carrier of n is non empty set

r is non empty TopSpace-like SubSpace of n

the carrier of r is non empty set

x is Element of the carrier of n

f is Element of the carrier of n

g is Element of the carrier of r

C is Element of the carrier of r

f2 is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total Path of x,f

x is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total Path of x,f

p is non empty Relation-like the carrier of I[01] -defined the carrier of r -valued Function-like total quasi_total Path of g,C

U is non empty Relation-like the carrier of I[01] -defined the carrier of r -valued Function-like total quasi_total Path of g,C

[: the carrier of [:I[01],I[01]:], the carrier of r:] is Relation-like set

bool [: the carrier of [:I[01],I[01]:], the carrier of r:] is set

V is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of r -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of r:]

[: the carrier of [:I[01],I[01]:], the carrier of n:] is Relation-like set

bool [: the carrier of [:I[01],I[01]:], the carrier of n:] is set

c is non empty Relation-like the carrier of [:I[01],I[01]:] -defined the carrier of n -valued Function-like total quasi_total Element of bool [: the carrier of [:I[01],I[01]:], the carrier of n:]

p . 0 is set

p . 1 is set

f2 . 0 is set

f2 . 1 is set

fc1 is real V101() ext-real Element of the carrier of I[01]

c . (fc1,0) is set

f2 . fc1 is Element of the carrier of n

fc2 is real V101() ext-real Element of the carrier of I[01]

c . (fc2,1) is set

x . fc2 is Element of the carrier of n

c0 is real V101() ext-real Element of the carrier of I[01]

c . (0,c0) is set

f0 is real V101() ext-real Element of the carrier of I[01]

c . (1,f0) is set

n is non empty TopSpace-like TopStruct

the carrier of n is non empty set

r is non empty TopSpace-like SubSpace of n

the carrier of r is non empty set

x is Element of the carrier of n

f is Element of the carrier of n

Paths (x,f) is non empty set

EqRel (n,x,f) is Relation-like Paths (x,f) -defined Paths (x,f) -valued Element of bool [:(Paths (x,f)),(Paths (x,f)):]

[:(Paths (x,f)),(Paths (x,f)):] is Relation-like set

bool [:(Paths (x,f)),(Paths (x,f)):] is set

g is Element of the carrier of r

C is Element of the carrier of r

Paths (g,C) is non empty set

EqRel (r,g,C) is Relation-like Paths (g,C) -defined Paths (g,C) -valued Element of bool [:(Paths (g,C)),(Paths (g,C)):]

[:(Paths (g,C)),(Paths (g,C)):] is Relation-like set

bool [:(Paths (g,C)),(Paths (g,C)):] is set

f2 is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total Path of x,f

x is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total Path of x,f

Class ((EqRel (n,x,f)),f2) is Element of bool (Paths (x,f))

bool (Paths (x,f)) is set

Class ((EqRel (n,x,f)),x) is Element of bool (Paths (x,f))

p is non empty Relation-like the carrier of I[01] -defined the carrier of r -valued Function-like total quasi_total Path of g,C

U is non empty Relation-like the carrier of I[01] -defined the carrier of r -valued Function-like total quasi_total Path of g,C

Class ((EqRel (r,g,C)),p) is Element of bool (Paths (g,C))

bool (Paths (g,C)) is set

Class ((EqRel (r,g,C)),U) is Element of bool (Paths (g,C))

n is non empty trivial finite 1 -element TopSpace-like pathwise_connected TopStruct

the carrier of n is non empty trivial finite set

r is Element of the carrier of n

FundamentalGroup (n,r) is non empty V116() V223() V224() V225() V253() V254() V255() V256() V257() V258() L10()

the carrier of (FundamentalGroup (n,r)) is non empty set

Loops r is non empty set

Paths (r,r) is non empty set

EqRel (n,r) is non empty Relation-like Loops r -defined Loops r -valued total quasi_total V70() V72() V77() Element of bool [:(Loops r),(Loops r):]

[:(Loops r),(Loops r):] is Relation-like set

bool [:(Loops r),(Loops r):] is set

EqRel (n,r,r) is Relation-like Paths (r,r) -defined Paths (r,r) -valued Element of bool [:(Paths (r,r)),(Paths (r,r)):]

[:(Paths (r,r)),(Paths (r,r)):] is Relation-like set

bool [:(Paths (r,r)),(Paths (r,r)):] is set

f is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total continuous Path of r,r

Class ((EqRel (n,r)),f) is Element of bool (Loops r)

bool (Loops r) is set

{(Class ((EqRel (n,r)),f))} is non empty trivial finite set

g is set

C is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total continuous Path of r,r

Class ((EqRel (n,r)),C) is Element of bool (Loops r)

I[01] --> r is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of n:]

[: the carrier of I[01], the carrier of n:] is Relation-like set

bool [: the carrier of I[01], the carrier of n:] is set

the carrier of I[01] --> r is non empty Relation-like the carrier of I[01] -defined the carrier of n -valued Function-like constant total quasi_total quasi_total continuous Element of bool [: the carrier of I[01], the carrier of n:]

g is set

Class (EqRel (n,r)) is a_partition of Loops r

n is ordinal natural real V101() ext-real non negative set

TOP-REAL n is non empty TopSpace-like V114() V142() V143() V144() V145() V146() V147() V148() strict V243() V244() n -locally_euclidean V359() RLTopStruct

the carrier of (TOP-REAL n) is non empty set

bool the carrier of (TOP-REAL n) is set

[#] (TOP-REAL n) is non empty non proper closed Element of bool the carrier of (TOP-REAL n)

r is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

{r} is non empty trivial functional finite V29() set

([#] (TOP-REAL n)) \ {r} is Element of bool the carrier of (TOP-REAL n)

x is Element of bool the carrier of (TOP-REAL n)

(TOP-REAL n) | x is strict TopSpace-like SubSpace of TOP-REAL n

f is non empty TopSpace-like SubSpace of TOP-REAL n

[#] f is non empty non proper closed Element of bool the carrier of f

the carrier of f is non empty set

bool the carrier of f is set

g is Element of the carrier of f

C is Element of the carrier of f

f2 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

x is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

LSeg (f2,x) is Element of bool the carrier of (TOP-REAL n)

(TOP-REAL n) | (LSeg (f2,x)) is strict TopSpace-like SubSpace of TOP-REAL n

[#] ((TOP-REAL n) | (LSeg (f2,x))) is non proper closed Element of bool the carrier of ((TOP-REAL n) | (LSeg (f2,x)))

the carrier of ((TOP-REAL n) | (LSeg (f2,x))) is set

bool the carrier of ((TOP-REAL n) | (LSeg (f2,x))) is set

p is non empty TopSpace-like SubSpace of f

the carrier of p is non empty set

[: the carrier of I[01], the carrier of p:] is Relation-like set

bool [: the carrier of I[01], the carrier of p:] is set

U is non empty Relation-like the carrier of I[01] -defined the carrier of p -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of p:]

U . 0 is set

U . 1 is set

[: the carrier of I[01], the carrier of f:] is Relation-like set

bool [: the carrier of I[01], the carrier of f:] is set

V is non empty Relation-like the carrier of I[01] -defined the carrier of f -valued Function-like total quasi_total Element of bool [: the carrier of I[01], the carrier of f:]

V . 0 is set

V . 1 is set

g is Element of the carrier of f

C is Element of the carrier of f

f2 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

x is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

LSeg (f2,x) is Element of bool the carrier of (TOP-REAL n)

p is ordinal natural real V101() ext-real non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT

TOP-REAL p is non empty TopSpace-like V114() V142() V143() V144() V145() V146() V147() V148() strict V243() V244() p -locally_euclidean V359() RLTopStruct

the carrier of (TOP-REAL p) is non empty set

U is Relation-like NAT -defined Function-like finite V32(p) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL p)

V is Relation-like NAT -defined Function-like finite V32(p) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL p)

c is real V101() ext-real Element of REAL

1 - c is real V101() ext-real set

(1 - c) * U is Relation-like NAT -defined Function-like finite V32(p) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL p)

(1 - c) * U is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

c * V is Relation-like NAT -defined Function-like finite V32(p) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL p)

c * V is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

((1 - c) * U) + (c * V) is Relation-like NAT -defined Function-like finite V32(p) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL p)

((1 - c) * U) + (c * V) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

x - f2 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

x - f2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

n - 1 is real V101() ext-real set

fc2 is ordinal natural real V101() ext-real non negative set

fc2 + 1 is non empty ordinal natural real V101() ext-real positive non negative V153() V154() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

TOP-REAL (fc2 + 1) is non empty non trivial non finite TopSpace-like V114() V142() V143() V144() V145() V146() V147() V148() strict V243() V244() fc2 + 1 -locally_euclidean V359() RLTopStruct

0. (TOP-REAL (fc2 + 1)) is Relation-like NAT -defined Function-like finite V32(fc2 + 1) V45( TOP-REAL (fc2 + 1)) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL (fc2 + 1))

the carrier of (TOP-REAL (fc2 + 1)) is non empty non trivial non finite set

the ZeroF of (TOP-REAL (fc2 + 1)) is Relation-like NAT -defined Function-like finite V32(fc2 + 1) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL (fc2 + 1))

TPlane ((x - f2),r) is non empty TopSpace-like SubSpace of TOP-REAL n

[#] (TPlane ((x - f2),r)) is non empty non proper closed Element of bool the carrier of (TPlane ((x - f2),r))

the carrier of (TPlane ((x - f2),r)) is non empty set

bool the carrier of (TPlane ((x - f2),r)) is set

Plane ((x - f2),r) is Element of bool the carrier of (TOP-REAL n)

(TOP-REAL n) | (Plane ((x - f2),r)) is strict TopSpace-like SubSpace of TOP-REAL n

[#] ((TOP-REAL n) | (Plane ((x - f2),r))) is non proper closed Element of bool the carrier of ((TOP-REAL n) | (Plane ((x - f2),r)))

the carrier of ((TOP-REAL n) | (Plane ((x - f2),r))) is set

bool the carrier of ((TOP-REAL n) | (Plane ((x - f2),r))) is set

c0 is set

c0 \ {r} is Element of bool c0

bool c0 is set

f0 is set

{ b

c1 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

c1 - r is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

c1 - r is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

|((x - f2),(c1 - r))| is real V101() ext-real Element of REAL

|((x - f2),(x - f2))| is real V101() ext-real Element of REAL

0. (TOP-REAL n) is Relation-like NAT -defined Function-like finite V32(n) V45( TOP-REAL n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

the ZeroF of (TOP-REAL n) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

LSeg (f2,c1) is Element of bool the carrier of (TOP-REAL n)

c2 is Relation-like NAT -defined Function-like finite V32(p) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL p)

ci1 is real V101() ext-real Element of REAL

1 - ci1 is real V101() ext-real set

(1 - ci1) * U is Relation-like NAT -defined Function-like finite V32(p) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL p)

(1 - ci1) * U is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

ci1 * c2 is Relation-like NAT -defined Function-like finite V32(p) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL p)

ci1 * c2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

((1 - ci1) * U) + (ci1 * c2) is Relation-like NAT -defined Function-like finite V32(p) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL p)

((1 - ci1) * U) + (ci1 * c2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

0. (TOP-REAL n) is Relation-like NAT -defined Function-like finite V32(n) V45( TOP-REAL n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

the ZeroF of (TOP-REAL n) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

1 * c1 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

1 * c1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(0. (TOP-REAL n)) + (1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(0. (TOP-REAL n)) + (1 * c1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(0. (TOP-REAL n)) + c1 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(0. (TOP-REAL n)) + c1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

c1 - f2 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

c1 - f2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(1 - ci1) * f2 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(1 - ci1) * f2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

c1 - ((1 - ci1) * f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

c1 - ((1 - ci1) * f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

ci1 * c1 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

ci1 * c1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(c1 - ((1 - ci1) * f2)) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(c1 - ((1 - ci1) * f2)) - (ci1 * c1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

- ((1 - ci1) * f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

- ((1 - ci1) * f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

c1 + (- ((1 - ci1) * f2)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

c1 + (- ((1 - ci1) * f2)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(c1 + (- ((1 - ci1) * f2))) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(c1 + (- ((1 - ci1) * f2))) - (ci1 * c1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

- (1 - ci1) is real V101() ext-real set

(- (1 - ci1)) * f2 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(- (1 - ci1)) * f2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

c1 + ((- (1 - ci1)) * f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

c1 + ((- (1 - ci1)) * f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(c1 + ((- (1 - ci1)) * f2)) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(c1 + ((- (1 - ci1)) * f2)) - (ci1 * c1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

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

(- 1) + ci1 is real V101() ext-real set

((- 1) + ci1) * f2 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

((- 1) + ci1) * f2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

c1 + (((- 1) + ci1) * f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

c1 + (((- 1) + ci1) * f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(c1 + (((- 1) + ci1) * f2)) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(c1 + (((- 1) + ci1) * f2)) - (ci1 * c1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(- 1) * f2 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(- 1) * f2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

ci1 * f2 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

ci1 * f2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

((- 1) * f2) + (ci1 * f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

((- 1) * f2) + (ci1 * f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

c1 + (((- 1) * f2) + (ci1 * f2)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

c1 + (((- 1) * f2) + (ci1 * f2)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(c1 + (((- 1) * f2) + (ci1 * f2))) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(c1 + (((- 1) * f2) + (ci1 * f2))) - (ci1 * c1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

- f2 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

- f2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(- f2) + (ci1 * f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(- f2) + (ci1 * f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

c1 + ((- f2) + (ci1 * f2)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

c1 + ((- f2) + (ci1 * f2)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(c1 + ((- f2) + (ci1 * f2))) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(c1 + ((- f2) + (ci1 * f2))) - (ci1 * c1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

c1 + (- f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

c1 + (- f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(c1 + (- f2)) + (ci1 * f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(c1 + (- f2)) + (ci1 * f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

((c1 + (- f2)) + (ci1 * f2)) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

((c1 + (- f2)) + (ci1 * f2)) - (ci1 * c1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(c1 - f2) + (ci1 * f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(c1 - f2) + (ci1 * f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

((c1 - f2) + (ci1 * f2)) - (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

((c1 - f2) + (ci1 * f2)) - (ci1 * c1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

- (ci1 * c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

- (ci1 * c1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

((c1 - f2) + (ci1 * f2)) + (- (ci1 * c1)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

((c1 - f2) + (ci1 * f2)) + (- (ci1 * c1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

- c1 is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

- c1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

ci1 * (- c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

ci1 * (- c1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

((c1 - f2) + (ci1 * f2)) + (ci1 * (- c1)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

((c1 - f2) + (ci1 * f2)) + (ci1 * (- c1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(ci1 * f2) + (ci1 * (- c1)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(ci1 * f2) + (ci1 * (- c1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(c1 - f2) + ((ci1 * f2) + (ci1 * (- c1))) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(c1 - f2) + ((ci1 * f2) + (ci1 * (- c1))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

f2 + (- c1) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

f2 + (- c1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

ci1 * (f2 + (- c1)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

ci1 * (f2 + (- c1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(c1 - f2) + (ci1 * (f2 + (- c1))) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(c1 - f2) + (ci1 * (f2 + (- c1))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

- (c1 - f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

- (c1 - f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

ci1 * (- (c1 - f2)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

ci1 * (- (c1 - f2)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(c1 - f2) + (ci1 * (- (c1 - f2))) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(c1 - f2) + (ci1 * (- (c1 - f2))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

ci1 * (c1 - f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

ci1 * (c1 - f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

- (ci1 * (c1 - f2)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

- (ci1 * (c1 - f2)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(c1 - f2) + (- (ci1 * (c1 - f2))) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(c1 - f2) + (- (ci1 * (c1 - f2))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

- ci1 is real V101() ext-real set

(- ci1) * (c1 - f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(- ci1) * (c1 - f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(c1 - f2) + ((- ci1) * (c1 - f2)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(c1 - f2) + ((- ci1) * (c1 - f2)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

1 * (c1 - f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

1 * (c1 - f2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

(1 * (c1 - f2)) + ((- ci1) * (c1 - f2)) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)

(1 * (c1 - f2)) + ((- ci1) * (c1 - f2)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued FinSequence of REAL

1 + (- ci1) is real V101() ext-real set

(1 + (- ci1)) * (c1 - f2) is Relation-like NAT -defined Function-like finite V32(n) FinSequence-like FinSubsequence-like complex-yielding ext-real-valued real-valued Element of the carrier of (TOP-REAL n)