REAL is non empty V54() V160() V161() V162() V166() set
NAT is V160() V161() V162() V163() V164() V165() V166() Element of K6(REAL)
K6(REAL) is set
K7(REAL,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is set
omega is V160() V161() V162() V163() V164() V165() V166() set
K6(omega) is set
K6(NAT) is set
K7(NAT,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(NAT,REAL)) is set
COMPLEX is non empty V54() V160() V166() set
RAT is non empty V54() V160() V161() V162() V163() V166() set
INT is non empty V54() V160() V161() V162() V163() V164() V166() set
1 is non empty ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
K7(1,1) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(1,1),REAL)) is set
K7(K7(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
K7(2,2) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K7(K7(2,2),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(2,2),REAL)) is set
K389(2) is V66() V92() V117() V118() V119() V120() V121() V122() V123() V172() V202() L20()
the U1 of K389(2) is set
REAL 1 is non empty FinSequence-membered M11( REAL )
K7((REAL 1),(REAL 1)) is set
K6(K7((REAL 1),(REAL 1))) is set
K400(1) is V66() V129() L15()
the U1 of K400(1) is set
K261(K400(1),K400(1)) is V66() L15()
the U1 of K261(K400(1),K400(1)) is set
REAL 2 is non empty FinSequence-membered M11( REAL )
K7((REAL 2),REAL) is complex-valued ext-real-valued real-valued set
K6(K7((REAL 2),REAL)) is set
K7(COMPLEX,COMPLEX) is complex-valued set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V20( RAT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(NAT,NAT),NAT)) is set
0 is empty ordinal natural V11() real ext-real non positive non negative V136() V159() V160() V161() V162() V163() V164() V165() V166() Element of NAT
proj (1,2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
proj (2,2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
{} is empty V160() V161() V162() V163() V164() V165() V166() set
f is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
z0 is non empty ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL z0 is non empty FinSequence-membered M11( REAL )
K7((REAL z0),REAL) is complex-valued ext-real-valued real-valued set
K6(K7((REAL z0),REAL)) is set
f is ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
f2 is V16() V19( REAL z0) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL z0),REAL))
h is non empty V16() V19( REAL z0) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL z0),REAL))
c is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(z0) FinSequence-like Element of REAL z0
h . c is V11() real ext-real Element of REAL
partdiff (f2,c,f) is V11() real ext-real Element of REAL
h is non empty V16() V19( REAL z0) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL z0),REAL))
c is non empty V16() V19( REAL z0) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL z0),REAL))
x0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(z0) FinSequence-like Element of REAL z0
h . x0 is V11() real ext-real Element of REAL
partdiff (f2,x0,f) is V11() real ext-real Element of REAL
c . x0 is V11() real ext-real Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
(1,2,f) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (1,(1,2,f),z0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,(1,2,f),z0)) is V160() V161() V162() Element of K6(REAL)
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
<*f2,h*> is set
(SVF1 (1,(1,2,f),z0)) . f2 is V11() real ext-real Element of REAL
c is V160() V161() V162() Neighbourhood of f2
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
c is V160() V161() V162() Neighbourhood of f2
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V11() real ext-real Element of REAL
x0 . 1 is V11() real ext-real Element of REAL
N * 1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
c is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
<*c,x0*> is set
y0 is V160() V161() V162() Neighbourhood of c
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
(SVF1 (1,(1,2,f),z0)) . c is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
c is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
<*c,x0*> is set
(SVF1 (1,(1,2,f),z0)) . c is V11() real ext-real Element of REAL
y0 is V160() V161() V162() Neighbourhood of c
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
y0 is V160() V161() V162() Neighbourhood of c
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R is V11() real ext-real Element of REAL
R * 1 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
N is V160() V161() V162() Neighbourhood of x0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
(SVF1 (1,(1,2,f),z0)) . x0 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
(SVF1 (1,(1,2,f),z0)) . x0 is V11() real ext-real Element of REAL
N is V160() V161() V162() Neighbourhood of x0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V160() V161() V162() Neighbourhood of x0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
r1 is V11() real ext-real Element of REAL
N0 is V160() V161() V162() Neighbourhood of x0
g is V11() real ext-real set
x0 - g is V11() real ext-real Element of REAL
x0 + g is V11() real ext-real Element of REAL
].(x0 - g),(x0 + g).[ is V160() V161() V162() Element of K6(REAL)
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= x0 - g & not x0 + g <= b1 ) } is set
s1 is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
h is ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
h + 2 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
g / (h + 2) is V11() real ext-real Element of REAL
s1 . h is V11() real ext-real Element of REAL
lim s1 is V11() real ext-real Element of REAL
h is V16() non-zero V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))
n is ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
h . n is V11() real ext-real Element of REAL
n + 2 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
g / (n + 2) is V11() real ext-real Element of REAL
x0 + (g / (n + 2)) is V11() real ext-real Element of REAL
(x0 + (g / (n + 2))) - x0 is V11() real ext-real Element of REAL
n + 1 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
(n + 1) + 1 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
0 + 1 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
g / 1 is V11() real ext-real Element of REAL
- g is V11() real ext-real set
x0 + (- g) is V11() real ext-real Element of REAL
r1 * 1 is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
(SVF1 (1,(1,2,f),z0)) . n is V11() real ext-real Element of REAL
((SVF1 (1,(1,2,f),z0)) . n) - ((SVF1 (1,(1,2,f),z0)) . x0) is V11() real ext-real Element of REAL
n - x0 is V11() real ext-real Element of REAL
L . (n - x0) is V11() real ext-real Element of REAL
R . (n - x0) is V11() real ext-real Element of REAL
(L . (n - x0)) + (R . (n - x0)) is V11() real ext-real Element of REAL
N . (n - x0) is V11() real ext-real Element of REAL
L . (n - x0) is V11() real ext-real Element of REAL
(N . (n - x0)) + (L . (n - x0)) is V11() real ext-real Element of REAL
r1 * (n - x0) is V11() real ext-real Element of REAL
(r1 * (n - x0)) + (R . (n - x0)) is V11() real ext-real Element of REAL
f2 * (n - x0) is V11() real ext-real Element of REAL
(f2 * (n - x0)) + (R . (n - x0)) is V11() real ext-real Element of REAL
h * (n - x0) is V11() real ext-real Element of REAL
(h * (n - x0)) + (L . (n - x0)) is V11() real ext-real Element of REAL
f2 - h is V11() real ext-real Element of REAL
h " is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
L /* h is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(h ") (#) (L /* h) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
R /* h is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(h ") (#) (R /* h) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((h ") (#) (L /* h)) - ((h ") (#) (R /* h)) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
dom L is V160() V161() V162() Element of K6(REAL)
rng h is V160() V161() V162() Element of K6(REAL)
n is ordinal natural V11() real ext-real non negative set
(((h ") (#) (L /* h)) - ((h ") (#) (R /* h))) . n is V11() real ext-real Element of REAL
dom R is V160() V161() V162() Element of K6(REAL)
h . n is V11() real ext-real Element of REAL
f2 * (h . n) is V11() real ext-real Element of REAL
R . (h . n) is V11() real ext-real Element of REAL
(f2 * (h . n)) + (R . (h . n)) is V11() real ext-real Element of REAL
h * (h . n) is V11() real ext-real Element of REAL
L . (h . n) is V11() real ext-real Element of REAL
(h * (h . n)) + (L . (h . n)) is V11() real ext-real Element of REAL
c22 is V11() real ext-real Element of REAL
c22 - x0 is V11() real ext-real Element of REAL
(f2 * (h . n)) / (h . n) is V11() real ext-real Element of REAL
(R . (h . n)) / (h . n) is V11() real ext-real Element of REAL
((f2 * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) is V11() real ext-real Element of REAL
((h * (h . n)) + (L . (h . n))) / (h . n) is V11() real ext-real Element of REAL
(h . n) " is V11() real ext-real Element of REAL
(R . (h . n)) * ((h . n) ") is V11() real ext-real Element of REAL
(h ") . n is V11() real ext-real Element of REAL
(R . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL
(R /* h) . n is V11() real ext-real Element of REAL
((R /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL
((h ") (#) (R /* h)) . n is V11() real ext-real Element of REAL
(L . (h . n)) / (h . n) is V11() real ext-real Element of REAL
(L . (h . n)) * ((h . n) ") is V11() real ext-real Element of REAL
(L . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL
(L /* h) . n is V11() real ext-real Element of REAL
((L /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL
((h ") (#) (L /* h)) . n is V11() real ext-real Element of REAL
(h * (h . n)) / (h . n) is V11() real ext-real Element of REAL
(h . n) / (h . n) is V11() real ext-real Element of REAL
h * ((h . n) / (h . n)) is V11() real ext-real Element of REAL
h * 1 is V11() real ext-real Element of REAL
f2 * ((h . n) / (h . n)) is V11() real ext-real Element of REAL
f2 * 1 is V11() real ext-real Element of REAL
f2 + ((R . (h . n)) / (h . n)) is V11() real ext-real Element of REAL
h + ((L . (h . n)) / (h . n)) is V11() real ext-real Element of REAL
(((h ") (#) (L /* h)) . n) - (((h ") (#) (R /* h)) . n) is V11() real ext-real Element of REAL
h + ((((h ") (#) (L /* h)) . n) - (((h ") (#) (R /* h)) . n)) is V11() real ext-real Element of REAL
(((h ") (#) (L /* h)) - ((h ") (#) (R /* h))) . 1 is V11() real ext-real Element of REAL
lim (((h ") (#) (L /* h)) - ((h ") (#) (R /* h))) is V11() real ext-real Element of REAL
lim ((h ") (#) (L /* h)) is V11() real ext-real Element of REAL
lim ((h ") (#) (R /* h)) is V11() real ext-real Element of REAL
0 - 0 is empty V11() real ext-real non positive non negative V160() V161() V162() V163() V164() V165() V166() Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
(1,2,f) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (2,(1,2,f),z0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,(1,2,f),z0)) is V160() V161() V162() Element of K6(REAL)
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
<*f2,h*> is set
(SVF1 (2,(1,2,f),z0)) . h is V11() real ext-real Element of REAL
c is V160() V161() V162() Neighbourhood of h
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
c is V160() V161() V162() Neighbourhood of h
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V11() real ext-real Element of REAL
x0 . 1 is V11() real ext-real Element of REAL
N * 1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
c is V11() real ext-real Element of REAL
<*c,x0*> is set
y0 is V160() V161() V162() Neighbourhood of x0
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
(SVF1 (2,(1,2,f),z0)) . x0 is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
c is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
<*c,x0*> is set
(SVF1 (2,(1,2,f),z0)) . x0 is V11() real ext-real Element of REAL
y0 is V160() V161() V162() Neighbourhood of x0
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
y0 is V160() V161() V162() Neighbourhood of x0
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R is V11() real ext-real Element of REAL
R * 1 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
N is V160() V161() V162() Neighbourhood of y0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
(SVF1 (2,(1,2,f),z0)) . y0 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
(SVF1 (2,(1,2,f),z0)) . y0 is V11() real ext-real Element of REAL
N is V160() V161() V162() Neighbourhood of y0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V160() V161() V162() Neighbourhood of y0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
r1 is V11() real ext-real Element of REAL
N0 is V160() V161() V162() Neighbourhood of y0
g is V11() real ext-real set
y0 - g is V11() real ext-real Element of REAL
y0 + g is V11() real ext-real Element of REAL
].(y0 - g),(y0 + g).[ is V160() V161() V162() Element of K6(REAL)
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= y0 - g & not y0 + g <= b1 ) } is set
s1 is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
h is ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
h + 2 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
g / (h + 2) is V11() real ext-real Element of REAL
s1 . h is V11() real ext-real Element of REAL
lim s1 is V11() real ext-real Element of REAL
h is V16() non-zero V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))
n is ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
h . n is V11() real ext-real Element of REAL
n + 2 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
g / (n + 2) is V11() real ext-real Element of REAL
y0 + (g / (n + 2)) is V11() real ext-real Element of REAL
(y0 + (g / (n + 2))) - y0 is V11() real ext-real Element of REAL
n + 1 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
(n + 1) + 1 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
0 + 1 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
g / 1 is V11() real ext-real Element of REAL
- g is V11() real ext-real set
y0 + (- g) is V11() real ext-real Element of REAL
r1 * 1 is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
(SVF1 (2,(1,2,f),z0)) . n is V11() real ext-real Element of REAL
((SVF1 (2,(1,2,f),z0)) . n) - ((SVF1 (2,(1,2,f),z0)) . y0) is V11() real ext-real Element of REAL
n - y0 is V11() real ext-real Element of REAL
L . (n - y0) is V11() real ext-real Element of REAL
R . (n - y0) is V11() real ext-real Element of REAL
(L . (n - y0)) + (R . (n - y0)) is V11() real ext-real Element of REAL
N . (n - y0) is V11() real ext-real Element of REAL
L . (n - y0) is V11() real ext-real Element of REAL
(N . (n - y0)) + (L . (n - y0)) is V11() real ext-real Element of REAL
r1 * (n - y0) is V11() real ext-real Element of REAL
(r1 * (n - y0)) + (R . (n - y0)) is V11() real ext-real Element of REAL
f2 * (n - y0) is V11() real ext-real Element of REAL
(f2 * (n - y0)) + (R . (n - y0)) is V11() real ext-real Element of REAL
h * (n - y0) is V11() real ext-real Element of REAL
(h * (n - y0)) + (L . (n - y0)) is V11() real ext-real Element of REAL
dom L is V160() V161() V162() Element of K6(REAL)
rng h is V160() V161() V162() Element of K6(REAL)
dom R is V160() V161() V162() Element of K6(REAL)
n is ordinal natural V11() real ext-real non negative set
h . n is V11() real ext-real Element of REAL
f2 * (h . n) is V11() real ext-real Element of REAL
R . (h . n) is V11() real ext-real Element of REAL
(f2 * (h . n)) + (R . (h . n)) is V11() real ext-real Element of REAL
h * (h . n) is V11() real ext-real Element of REAL
L . (h . n) is V11() real ext-real Element of REAL
(h * (h . n)) + (L . (h . n)) is V11() real ext-real Element of REAL
c22 is V11() real ext-real Element of REAL
c22 - y0 is V11() real ext-real Element of REAL
(f2 * (h . n)) / (h . n) is V11() real ext-real Element of REAL
(R . (h . n)) / (h . n) is V11() real ext-real Element of REAL
((f2 * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) is V11() real ext-real Element of REAL
((h * (h . n)) + (L . (h . n))) / (h . n) is V11() real ext-real Element of REAL
(h . n) " is V11() real ext-real Element of REAL
(R . (h . n)) * ((h . n) ") is V11() real ext-real Element of REAL
h " is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(h ") . n is V11() real ext-real Element of REAL
(R . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL
R /* h is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(R /* h) . n is V11() real ext-real Element of REAL
((R /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL
(h ") (#) (R /* h) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((h ") (#) (R /* h)) . n is V11() real ext-real Element of REAL
(L . (h . n)) / (h . n) is V11() real ext-real Element of REAL
(L . (h . n)) * ((h . n) ") is V11() real ext-real Element of REAL
(L . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL
L /* h is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(L /* h) . n is V11() real ext-real Element of REAL
((L /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL
(h ") (#) (L /* h) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((h ") (#) (L /* h)) . n is V11() real ext-real Element of REAL
(h * (h . n)) / (h . n) is V11() real ext-real Element of REAL
(h . n) / (h . n) is V11() real ext-real Element of REAL
h * ((h . n) / (h . n)) is V11() real ext-real Element of REAL
h * 1 is V11() real ext-real Element of REAL
f2 * ((h . n) / (h . n)) is V11() real ext-real Element of REAL
f2 * 1 is V11() real ext-real Element of REAL
f2 + ((R . (h . n)) / (h . n)) is V11() real ext-real Element of REAL
h + ((L . (h . n)) / (h . n)) is V11() real ext-real Element of REAL
(((h ") (#) (L /* h)) . n) - (((h ") (#) (R /* h)) . n) is V11() real ext-real Element of REAL
h + ((((h ") (#) (L /* h)) . n) - (((h ") (#) (R /* h)) . n)) is V11() real ext-real Element of REAL
f2 - h is V11() real ext-real Element of REAL
((h ") (#) (L /* h)) - ((h ") (#) (R /* h)) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(((h ") (#) (L /* h)) - ((h ") (#) (R /* h))) . n is V11() real ext-real Element of REAL
(((h ") (#) (L /* h)) - ((h ") (#) (R /* h))) . 1 is V11() real ext-real Element of REAL
lim (((h ") (#) (L /* h)) - ((h ") (#) (R /* h))) is V11() real ext-real Element of REAL
lim ((h ") (#) (L /* h)) is V11() real ext-real Element of REAL
lim ((h ") (#) (R /* h)) is V11() real ext-real Element of REAL
0 - 0 is empty V11() real ext-real non positive non negative V160() V161() V162() V163() V164() V165() V166() Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
(2,2,f) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (1,(2,2,f),z0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,(2,2,f),z0)) is V160() V161() V162() Element of K6(REAL)
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
<*f2,h*> is set
(SVF1 (1,(2,2,f),z0)) . f2 is V11() real ext-real Element of REAL
c is V160() V161() V162() Neighbourhood of f2
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
c is V160() V161() V162() Neighbourhood of f2
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V11() real ext-real Element of REAL
x0 . 1 is V11() real ext-real Element of REAL
N * 1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
c is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
<*c,x0*> is set
y0 is V160() V161() V162() Neighbourhood of c
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
(SVF1 (1,(2,2,f),z0)) . c is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
c is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
<*c,x0*> is set
(SVF1 (1,(2,2,f),z0)) . c is V11() real ext-real Element of REAL
y0 is V160() V161() V162() Neighbourhood of c
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
y0 is V160() V161() V162() Neighbourhood of c
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R is V11() real ext-real Element of REAL
R * 1 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
N is V160() V161() V162() Neighbourhood of x0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
(SVF1 (1,(2,2,f),z0)) . x0 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
(SVF1 (1,(2,2,f),z0)) . x0 is V11() real ext-real Element of REAL
N is V160() V161() V162() Neighbourhood of x0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V160() V161() V162() Neighbourhood of x0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
r1 is V11() real ext-real Element of REAL
N0 is V160() V161() V162() Neighbourhood of x0
g is V11() real ext-real set
x0 - g is V11() real ext-real Element of REAL
x0 + g is V11() real ext-real Element of REAL
].(x0 - g),(x0 + g).[ is V160() V161() V162() Element of K6(REAL)
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= x0 - g & not x0 + g <= b1 ) } is set
s1 is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
h is ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
h + 2 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
g / (h + 2) is V11() real ext-real Element of REAL
s1 . h is V11() real ext-real Element of REAL
lim s1 is V11() real ext-real Element of REAL
h is V16() non-zero V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))
n is ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
h . n is V11() real ext-real Element of REAL
n + 2 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
g / (n + 2) is V11() real ext-real Element of REAL
x0 + (g / (n + 2)) is V11() real ext-real Element of REAL
(x0 + (g / (n + 2))) - x0 is V11() real ext-real Element of REAL
n + 1 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
(n + 1) + 1 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
0 + 1 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
g / 1 is V11() real ext-real Element of REAL
- g is V11() real ext-real set
x0 + (- g) is V11() real ext-real Element of REAL
r1 * 1 is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
(SVF1 (1,(2,2,f),z0)) . n is V11() real ext-real Element of REAL
((SVF1 (1,(2,2,f),z0)) . n) - ((SVF1 (1,(2,2,f),z0)) . x0) is V11() real ext-real Element of REAL
n - x0 is V11() real ext-real Element of REAL
L . (n - x0) is V11() real ext-real Element of REAL
R . (n - x0) is V11() real ext-real Element of REAL
(L . (n - x0)) + (R . (n - x0)) is V11() real ext-real Element of REAL
N . (n - x0) is V11() real ext-real Element of REAL
L . (n - x0) is V11() real ext-real Element of REAL
(N . (n - x0)) + (L . (n - x0)) is V11() real ext-real Element of REAL
r1 * (n - x0) is V11() real ext-real Element of REAL
(r1 * (n - x0)) + (R . (n - x0)) is V11() real ext-real Element of REAL
f2 * (n - x0) is V11() real ext-real Element of REAL
(f2 * (n - x0)) + (R . (n - x0)) is V11() real ext-real Element of REAL
h * (n - x0) is V11() real ext-real Element of REAL
(h * (n - x0)) + (L . (n - x0)) is V11() real ext-real Element of REAL
dom L is V160() V161() V162() Element of K6(REAL)
rng h is V160() V161() V162() Element of K6(REAL)
dom R is V160() V161() V162() Element of K6(REAL)
n is ordinal natural V11() real ext-real non negative set
h . n is V11() real ext-real Element of REAL
f2 * (h . n) is V11() real ext-real Element of REAL
R . (h . n) is V11() real ext-real Element of REAL
(f2 * (h . n)) + (R . (h . n)) is V11() real ext-real Element of REAL
h * (h . n) is V11() real ext-real Element of REAL
L . (h . n) is V11() real ext-real Element of REAL
(h * (h . n)) + (L . (h . n)) is V11() real ext-real Element of REAL
c22 is V11() real ext-real Element of REAL
c22 - x0 is V11() real ext-real Element of REAL
(f2 * (h . n)) / (h . n) is V11() real ext-real Element of REAL
(R . (h . n)) / (h . n) is V11() real ext-real Element of REAL
((f2 * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) is V11() real ext-real Element of REAL
((h * (h . n)) + (L . (h . n))) / (h . n) is V11() real ext-real Element of REAL
(h . n) " is V11() real ext-real Element of REAL
(R . (h . n)) * ((h . n) ") is V11() real ext-real Element of REAL
h " is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(h ") . n is V11() real ext-real Element of REAL
(R . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL
R /* h is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(R /* h) . n is V11() real ext-real Element of REAL
((R /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL
(h ") (#) (R /* h) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((h ") (#) (R /* h)) . n is V11() real ext-real Element of REAL
(L . (h . n)) / (h . n) is V11() real ext-real Element of REAL
(L . (h . n)) * ((h . n) ") is V11() real ext-real Element of REAL
(L . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL
L /* h is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(L /* h) . n is V11() real ext-real Element of REAL
((L /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL
(h ") (#) (L /* h) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((h ") (#) (L /* h)) . n is V11() real ext-real Element of REAL
(h * (h . n)) / (h . n) is V11() real ext-real Element of REAL
(h . n) / (h . n) is V11() real ext-real Element of REAL
h * ((h . n) / (h . n)) is V11() real ext-real Element of REAL
h * 1 is V11() real ext-real Element of REAL
f2 * ((h . n) / (h . n)) is V11() real ext-real Element of REAL
f2 * 1 is V11() real ext-real Element of REAL
f2 + ((R . (h . n)) / (h . n)) is V11() real ext-real Element of REAL
h + ((L . (h . n)) / (h . n)) is V11() real ext-real Element of REAL
(((h ") (#) (L /* h)) . n) - (((h ") (#) (R /* h)) . n) is V11() real ext-real Element of REAL
h + ((((h ") (#) (L /* h)) . n) - (((h ") (#) (R /* h)) . n)) is V11() real ext-real Element of REAL
f2 - h is V11() real ext-real Element of REAL
((h ") (#) (L /* h)) - ((h ") (#) (R /* h)) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(((h ") (#) (L /* h)) - ((h ") (#) (R /* h))) . n is V11() real ext-real Element of REAL
(((h ") (#) (L /* h)) - ((h ") (#) (R /* h))) . 1 is V11() real ext-real Element of REAL
lim (((h ") (#) (L /* h)) - ((h ") (#) (R /* h))) is V11() real ext-real Element of REAL
lim ((h ") (#) (L /* h)) is V11() real ext-real Element of REAL
lim ((h ") (#) (R /* h)) is V11() real ext-real Element of REAL
0 - 0 is empty V11() real ext-real non positive non negative V160() V161() V162() V163() V164() V165() V166() Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
(2,2,f) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (2,(2,2,f),z0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,(2,2,f),z0)) is V160() V161() V162() Element of K6(REAL)
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
<*f2,h*> is set
(SVF1 (2,(2,2,f),z0)) . h is V11() real ext-real Element of REAL
c is V160() V161() V162() Neighbourhood of h
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
c is V160() V161() V162() Neighbourhood of h
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V11() real ext-real Element of REAL
x0 . 1 is V11() real ext-real Element of REAL
N * 1 is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
c is V11() real ext-real Element of REAL
<*c,x0*> is set
y0 is V160() V161() V162() Neighbourhood of x0
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
(SVF1 (2,(2,2,f),z0)) . x0 is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
c is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
<*c,x0*> is set
(SVF1 (2,(2,2,f),z0)) . x0 is V11() real ext-real Element of REAL
y0 is V160() V161() V162() Neighbourhood of x0
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
y0 is V160() V161() V162() Neighbourhood of x0
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
N . 1 is V11() real ext-real Element of REAL
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R is V11() real ext-real Element of REAL
R * 1 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
N is V160() V161() V162() Neighbourhood of y0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
(SVF1 (2,(2,2,f),z0)) . y0 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
(SVF1 (2,(2,2,f),z0)) . y0 is V11() real ext-real Element of REAL
N is V160() V161() V162() Neighbourhood of y0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V160() V161() V162() Neighbourhood of y0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
r1 is V11() real ext-real Element of REAL
N0 is V160() V161() V162() Neighbourhood of y0
g is V11() real ext-real set
y0 - g is V11() real ext-real Element of REAL
y0 + g is V11() real ext-real Element of REAL
].(y0 - g),(y0 + g).[ is V160() V161() V162() Element of K6(REAL)
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= y0 - g & not y0 + g <= b1 ) } is set
s1 is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
h is ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
h + 2 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
g / (h + 2) is V11() real ext-real Element of REAL
s1 . h is V11() real ext-real Element of REAL
lim s1 is V11() real ext-real Element of REAL
h is V16() non-zero V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))
n is ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
h . n is V11() real ext-real Element of REAL
n + 2 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
g / (n + 2) is V11() real ext-real Element of REAL
y0 + (g / (n + 2)) is V11() real ext-real Element of REAL
(y0 + (g / (n + 2))) - y0 is V11() real ext-real Element of REAL
n + 1 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
(n + 1) + 1 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
0 + 1 is non empty ordinal natural V11() real ext-real positive non negative Element of REAL
g / 1 is V11() real ext-real Element of REAL
- g is V11() real ext-real set
y0 + (- g) is V11() real ext-real Element of REAL
r1 * 1 is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
(SVF1 (2,(2,2,f),z0)) . n is V11() real ext-real Element of REAL
((SVF1 (2,(2,2,f),z0)) . n) - ((SVF1 (2,(2,2,f),z0)) . y0) is V11() real ext-real Element of REAL
n - y0 is V11() real ext-real Element of REAL
L . (n - y0) is V11() real ext-real Element of REAL
R . (n - y0) is V11() real ext-real Element of REAL
(L . (n - y0)) + (R . (n - y0)) is V11() real ext-real Element of REAL
N . (n - y0) is V11() real ext-real Element of REAL
L . (n - y0) is V11() real ext-real Element of REAL
(N . (n - y0)) + (L . (n - y0)) is V11() real ext-real Element of REAL
r1 * (n - y0) is V11() real ext-real Element of REAL
(r1 * (n - y0)) + (R . (n - y0)) is V11() real ext-real Element of REAL
f2 * (n - y0) is V11() real ext-real Element of REAL
(f2 * (n - y0)) + (R . (n - y0)) is V11() real ext-real Element of REAL
h * (n - y0) is V11() real ext-real Element of REAL
(h * (n - y0)) + (L . (n - y0)) is V11() real ext-real Element of REAL
dom L is V160() V161() V162() Element of K6(REAL)
rng h is V160() V161() V162() Element of K6(REAL)
dom R is V160() V161() V162() Element of K6(REAL)
n is ordinal natural V11() real ext-real non negative set
h . n is V11() real ext-real Element of REAL
f2 * (h . n) is V11() real ext-real Element of REAL
R . (h . n) is V11() real ext-real Element of REAL
(f2 * (h . n)) + (R . (h . n)) is V11() real ext-real Element of REAL
h * (h . n) is V11() real ext-real Element of REAL
L . (h . n) is V11() real ext-real Element of REAL
(h * (h . n)) + (L . (h . n)) is V11() real ext-real Element of REAL
c22 is V11() real ext-real Element of REAL
c22 - y0 is V11() real ext-real Element of REAL
(f2 * (h . n)) / (h . n) is V11() real ext-real Element of REAL
(R . (h . n)) / (h . n) is V11() real ext-real Element of REAL
((f2 * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) is V11() real ext-real Element of REAL
((h * (h . n)) + (L . (h . n))) / (h . n) is V11() real ext-real Element of REAL
(h . n) " is V11() real ext-real Element of REAL
(R . (h . n)) * ((h . n) ") is V11() real ext-real Element of REAL
h " is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(h ") . n is V11() real ext-real Element of REAL
(R . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL
R /* h is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(R /* h) . n is V11() real ext-real Element of REAL
((R /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL
(h ") (#) (R /* h) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((h ") (#) (R /* h)) . n is V11() real ext-real Element of REAL
(L . (h . n)) / (h . n) is V11() real ext-real Element of REAL
(L . (h . n)) * ((h . n) ") is V11() real ext-real Element of REAL
(L . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL
L /* h is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(L /* h) . n is V11() real ext-real Element of REAL
((L /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL
(h ") (#) (L /* h) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((h ") (#) (L /* h)) . n is V11() real ext-real Element of REAL
(h * (h . n)) / (h . n) is V11() real ext-real Element of REAL
(h . n) / (h . n) is V11() real ext-real Element of REAL
h * ((h . n) / (h . n)) is V11() real ext-real Element of REAL
h * 1 is V11() real ext-real Element of REAL
f2 * ((h . n) / (h . n)) is V11() real ext-real Element of REAL
f2 * 1 is V11() real ext-real Element of REAL
f2 + ((R . (h . n)) / (h . n)) is V11() real ext-real Element of REAL
h + ((L . (h . n)) / (h . n)) is V11() real ext-real Element of REAL
(((h ") (#) (L /* h)) . n) - (((h ") (#) (R /* h)) . n) is V11() real ext-real Element of REAL
h + ((((h ") (#) (L /* h)) . n) - (((h ") (#) (R /* h)) . n)) is V11() real ext-real Element of REAL
f2 - h is V11() real ext-real Element of REAL
((h ") (#) (L /* h)) - ((h ") (#) (R /* h)) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(((h ") (#) (L /* h)) - ((h ") (#) (R /* h))) . n is V11() real ext-real Element of REAL
(((h ") (#) (L /* h)) - ((h ") (#) (R /* h))) . 1 is V11() real ext-real Element of REAL
lim (((h ") (#) (L /* h)) - ((h ") (#) (R /* h))) is V11() real ext-real Element of REAL
lim ((h ") (#) (L /* h)) is V11() real ext-real Element of REAL
lim ((h ") (#) (R /* h)) is V11() real ext-real Element of REAL
0 - 0 is empty V11() real ext-real non positive non negative V160() V161() V162() V163() V164() V165() V166() Element of REAL
f is V11() real ext-real Element of REAL
z0 is V11() real ext-real Element of REAL
<*f,z0*> is set
f2 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
h is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,h) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (1,(1,2,h),f2) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,(1,2,h),f2)) is V160() V161() V162() Element of K6(REAL)
c is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
<*c,x0*> is set
(SVF1 (1,(1,2,h),f2)) . c is V11() real ext-real Element of REAL
y0 is V160() V161() V162() Neighbourhood of c
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
f is V11() real ext-real Element of REAL
z0 is V11() real ext-real Element of REAL
<*f,z0*> is set
f2 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
h is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,h) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (2,(1,2,h),f2) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,(1,2,h),f2)) is V160() V161() V162() Element of K6(REAL)
c is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
<*c,x0*> is set
(SVF1 (2,(1,2,h),f2)) . x0 is V11() real ext-real Element of REAL
y0 is V160() V161() V162() Neighbourhood of x0
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
f is V11() real ext-real Element of REAL
z0 is V11() real ext-real Element of REAL
<*f,z0*> is set
f2 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
h is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,h) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (1,(2,2,h),f2) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,(2,2,h),f2)) is V160() V161() V162() Element of K6(REAL)
c is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
<*c,x0*> is set
(SVF1 (1,(2,2,h),f2)) . c is V11() real ext-real Element of REAL
y0 is V160() V161() V162() Neighbourhood of c
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
f is V11() real ext-real Element of REAL
z0 is V11() real ext-real Element of REAL
<*f,z0*> is set
f2 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
h is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,h) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (2,(2,2,h),f2) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,(2,2,h),f2)) is V160() V161() V162() Element of K6(REAL)
c is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
<*c,x0*> is set
(SVF1 (2,(2,2,h),f2)) . x0 is V11() real ext-real Element of REAL
y0 is V160() V161() V162() Neighbourhood of x0
N is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
f is V11() real ext-real Element of REAL
z0 is V11() real ext-real Element of REAL
<*f,z0*> is set
f2 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
h is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(h,f2) is V11() real ext-real Element of REAL
(1,2,h) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (1,(1,2,h),f2) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
diff ((SVF1 (1,(1,2,h),f2)),f) is V11() real ext-real Element of REAL
dom (SVF1 (1,(1,2,h),f2)) is V160() V161() V162() Element of K6(REAL)
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
(SVF1 (1,(1,2,h),f2)) . x0 is V11() real ext-real Element of REAL
N is V160() V161() V162() Neighbourhood of x0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V160() V161() V162() Neighbourhood of x0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
z0 is V11() real ext-real Element of REAL
<*f,z0*> is set
f2 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
h is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(h,f2) is V11() real ext-real Element of REAL
(1,2,h) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (2,(1,2,h),f2) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
diff ((SVF1 (2,(1,2,h),f2)),z0) is V11() real ext-real Element of REAL
dom (SVF1 (2,(1,2,h),f2)) is V160() V161() V162() Element of K6(REAL)
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
(SVF1 (2,(1,2,h),f2)) . y0 is V11() real ext-real Element of REAL
N is V160() V161() V162() Neighbourhood of y0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V160() V161() V162() Neighbourhood of y0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
z0 is V11() real ext-real Element of REAL
<*f,z0*> is set
f2 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
h is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(h,f2) is V11() real ext-real Element of REAL
(2,2,h) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (1,(2,2,h),f2) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
diff ((SVF1 (1,(2,2,h),f2)),f) is V11() real ext-real Element of REAL
dom (SVF1 (1,(2,2,h),f2)) is V160() V161() V162() Element of K6(REAL)
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
(SVF1 (1,(2,2,h),f2)) . x0 is V11() real ext-real Element of REAL
N is V160() V161() V162() Neighbourhood of x0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V160() V161() V162() Neighbourhood of x0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
z0 is V11() real ext-real Element of REAL
<*f,z0*> is set
f2 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
h is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(h,f2) is V11() real ext-real Element of REAL
(2,2,h) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (2,(2,2,h),f2) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
diff ((SVF1 (2,(2,2,h),f2)),z0) is V11() real ext-real Element of REAL
dom (SVF1 (2,(2,2,h),f2)) is V160() V161() V162() Element of K6(REAL)
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
(SVF1 (2,(2,2,h),f2)) . y0 is V11() real ext-real Element of REAL
N is V160() V161() V162() Neighbourhood of y0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V160() V161() V162() Neighbourhood of y0
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L . 1 is V11() real ext-real Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is set
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
dom f2 is Element of K6((REAL 2))
K6((REAL 2)) is set
dom f is Element of K6((REAL 2))
h is set
h is set
h is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
f2 . h is V11() real ext-real Element of REAL
(f,h) is V11() real ext-real Element of REAL
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
dom f2 is Element of K6((REAL 2))
K6((REAL 2)) is set
h is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
dom h is Element of K6((REAL 2))
c is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
f2 . c is V11() real ext-real Element of REAL
(f,c) is V11() real ext-real Element of REAL
h . c is V11() real ext-real Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is set
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
dom f2 is Element of K6((REAL 2))
K6((REAL 2)) is set
dom f is Element of K6((REAL 2))
h is set
h is set
h is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
f2 . h is V11() real ext-real Element of REAL
(f,h) is V11() real ext-real Element of REAL
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
dom f2 is Element of K6((REAL 2))
K6((REAL 2)) is set
h is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
dom h is Element of K6((REAL 2))
c is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
f2 . c is V11() real ext-real Element of REAL
(f,c) is V11() real ext-real Element of REAL
h . c is V11() real ext-real Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is set
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
dom f2 is Element of K6((REAL 2))
K6((REAL 2)) is set
dom f is Element of K6((REAL 2))
h is set
h is set
h is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
f2 . h is V11() real ext-real Element of REAL
(f,h) is V11() real ext-real Element of REAL
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
dom f2 is Element of K6((REAL 2))
K6((REAL 2)) is set
h is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
dom h is Element of K6((REAL 2))
c is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
f2 . c is V11() real ext-real Element of REAL
(f,c) is V11() real ext-real Element of REAL
h . c is V11() real ext-real Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is set
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
dom f2 is Element of K6((REAL 2))
K6((REAL 2)) is set
dom f is Element of K6((REAL 2))
h is set
h is set
h is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
f2 . h is V11() real ext-real Element of REAL
(f,h) is V11() real ext-real Element of REAL
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
dom f2 is Element of K6((REAL 2))
K6((REAL 2)) is set
h is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
dom h is Element of K6((REAL 2))
c is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
f2 . c is V11() real ext-real Element of REAL
(f,c) is V11() real ext-real Element of REAL
h . c is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (1,(1,2,z0),f) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,(1,2,z0),f)) is V160() V161() V162() Element of K6(REAL)
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
<*f2,h*> is set
c is V160() V161() V162() Neighbourhood of f2
(SVF1 (1,(1,2,z0),f)) . f2 is V11() real ext-real Element of REAL
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
SVF1 (1,(1,2,z0),f) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,(1,2,z0),f)) is V160() V161() V162() Element of K6(REAL)
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
<*f2,h*> is set
c is V160() V161() V162() Neighbourhood of f2
(SVF1 (1,(1,2,z0),f)) . f2 is V11() real ext-real Element of REAL
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (2,(1,2,z0),f) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,(1,2,z0),f)) is V160() V161() V162() Element of K6(REAL)
h is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*f2,h*> is set
c is V160() V161() V162() Neighbourhood of h
(SVF1 (2,(1,2,z0),f)) . h is V11() real ext-real Element of REAL
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
SVF1 (2,(1,2,z0),f) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,(1,2,z0),f)) is V160() V161() V162() Element of K6(REAL)
h is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*f2,h*> is set
c is V160() V161() V162() Neighbourhood of h
(SVF1 (2,(1,2,z0),f)) . h is V11() real ext-real Element of REAL
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (1,(2,2,z0),f) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,(2,2,z0),f)) is V160() V161() V162() Element of K6(REAL)
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
<*f2,h*> is set
c is V160() V161() V162() Neighbourhood of f2
(SVF1 (1,(2,2,z0),f)) . f2 is V11() real ext-real Element of REAL
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
SVF1 (1,(2,2,z0),f) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,(2,2,z0),f)) is V160() V161() V162() Element of K6(REAL)
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
<*f2,h*> is set
c is V160() V161() V162() Neighbourhood of f2
(SVF1 (1,(2,2,z0),f)) . f2 is V11() real ext-real Element of REAL
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
SVF1 (2,(2,2,z0),f) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,(2,2,z0),f)) is V160() V161() V162() Element of K6(REAL)
h is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*f2,h*> is set
c is V160() V161() V162() Neighbourhood of h
(SVF1 (2,(2,2,z0),f)) . h is V11() real ext-real Element of REAL
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
SVF1 (2,(2,2,z0),f) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,(2,2,z0),f)) is V160() V161() V162() Element of K6(REAL)
h is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
<*f2,h*> is set
c is V160() V161() V162() Neighbourhood of h
(SVF1 (2,(2,2,z0),f)) . h is V11() real ext-real Element of REAL
x0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
y0 is non empty V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(z0,f) is V11() real ext-real Element of REAL
(1,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff ((1,2,z0),f,1) is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
<*f2,h*> is set
SVF1 (1,(1,2,z0),f) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
diff ((SVF1 (1,(1,2,z0),f)),f2) is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(z0,f) is V11() real ext-real Element of REAL
(1,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff ((1,2,z0),f,2) is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
<*f2,h*> is set
SVF1 (2,(1,2,z0),f) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
diff ((SVF1 (2,(1,2,z0),f)),h) is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(z0,f) is V11() real ext-real Element of REAL
(2,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff ((2,2,z0),f,1) is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
<*f2,h*> is set
SVF1 (1,(2,2,z0),f) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
diff ((SVF1 (1,(2,2,z0),f)),f2) is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(z0,f) is V11() real ext-real Element of REAL
(2,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff ((2,2,z0),f,2) is V11() real ext-real Element of REAL
f2 is V11() real ext-real Element of REAL
h is V11() real ext-real Element of REAL
<*f2,h*> is set
SVF1 (2,(2,2,z0),f) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
diff ((SVF1 (2,(2,2,z0),f)),h) is V11() real ext-real Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,f) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
(proj (1,2)) . z0 is V11() real ext-real Element of REAL
SVF1 (1,(1,2,f),z0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,(1,2,f),z0)) is V160() V161() V162() Element of K6(REAL)
{((proj (1,2)) . z0)} is non empty V160() V161() V162() set
(f,z0) is V11() real ext-real Element of REAL
f2 is V160() V161() V162() Neighbourhood of (proj (1,2)) . z0
h is V16() non-zero V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))
h " is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
c is V16() V19( NAT ) V20( REAL ) V21() constant total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng c is V160() V161() V162() Element of K6(REAL)
h + c is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng (h + c) is V160() V161() V162() Element of K6(REAL)
(SVF1 (1,(1,2,f),z0)) /* (h + c) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(SVF1 (1,(1,2,f),z0)) /* c is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((SVF1 (1,(1,2,f),z0)) /* (h + c)) - ((SVF1 (1,(1,2,f),z0)) /* c) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(h ") (#) (((SVF1 (1,(1,2,f),z0)) /* (h + c)) - ((SVF1 (1,(1,2,f),z0)) /* c)) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim ((h ") (#) (((SVF1 (1,(1,2,f),z0)) /* (h + c)) - ((SVF1 (1,(1,2,f),z0)) /* c))) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
partdiff ((1,2,f),z0,1) is V11() real ext-real Element of REAL
diff ((SVF1 (1,(1,2,f),z0)),x0) is V11() real ext-real Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,f) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
(proj (2,2)) . z0 is V11() real ext-real Element of REAL
SVF1 (2,(1,2,f),z0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,(1,2,f),z0)) is V160() V161() V162() Element of K6(REAL)
{((proj (2,2)) . z0)} is non empty V160() V161() V162() set
(f,z0) is V11() real ext-real Element of REAL
f2 is V160() V161() V162() Neighbourhood of (proj (2,2)) . z0
h is V16() non-zero V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))
h " is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
c is V16() V19( NAT ) V20( REAL ) V21() constant total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng c is V160() V161() V162() Element of K6(REAL)
h + c is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng (h + c) is V160() V161() V162() Element of K6(REAL)
(SVF1 (2,(1,2,f),z0)) /* (h + c) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(SVF1 (2,(1,2,f),z0)) /* c is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((SVF1 (2,(1,2,f),z0)) /* (h + c)) - ((SVF1 (2,(1,2,f),z0)) /* c) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(h ") (#) (((SVF1 (2,(1,2,f),z0)) /* (h + c)) - ((SVF1 (2,(1,2,f),z0)) /* c)) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim ((h ") (#) (((SVF1 (2,(1,2,f),z0)) /* (h + c)) - ((SVF1 (2,(1,2,f),z0)) /* c))) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
partdiff ((1,2,f),z0,2) is V11() real ext-real Element of REAL
diff ((SVF1 (2,(1,2,f),z0)),y0) is V11() real ext-real Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,f) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
(proj (1,2)) . z0 is V11() real ext-real Element of REAL
SVF1 (1,(2,2,f),z0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (1,(2,2,f),z0)) is V160() V161() V162() Element of K6(REAL)
{((proj (1,2)) . z0)} is non empty V160() V161() V162() set
(f,z0) is V11() real ext-real Element of REAL
f2 is V160() V161() V162() Neighbourhood of (proj (1,2)) . z0
h is V16() non-zero V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))
h " is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
c is V16() V19( NAT ) V20( REAL ) V21() constant total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng c is V160() V161() V162() Element of K6(REAL)
h + c is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng (h + c) is V160() V161() V162() Element of K6(REAL)
(SVF1 (1,(2,2,f),z0)) /* (h + c) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(SVF1 (1,(2,2,f),z0)) /* c is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((SVF1 (1,(2,2,f),z0)) /* (h + c)) - ((SVF1 (1,(2,2,f),z0)) /* c) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(h ") (#) (((SVF1 (1,(2,2,f),z0)) /* (h + c)) - ((SVF1 (1,(2,2,f),z0)) /* c)) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim ((h ") (#) (((SVF1 (1,(2,2,f),z0)) /* (h + c)) - ((SVF1 (1,(2,2,f),z0)) /* c))) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
partdiff ((2,2,f),z0,1) is V11() real ext-real Element of REAL
diff ((SVF1 (1,(2,2,f),z0)),x0) is V11() real ext-real Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,f) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
(proj (2,2)) . z0 is V11() real ext-real Element of REAL
SVF1 (2,(2,2,f),z0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (SVF1 (2,(2,2,f),z0)) is V160() V161() V162() Element of K6(REAL)
{((proj (2,2)) . z0)} is non empty V160() V161() V162() set
(f,z0) is V11() real ext-real Element of REAL
f2 is V160() V161() V162() Neighbourhood of (proj (2,2)) . z0
h is V16() non-zero V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))
h " is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
c is V16() V19( NAT ) V20( REAL ) V21() constant total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng c is V160() V161() V162() Element of K6(REAL)
h + c is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng (h + c) is V160() V161() V162() Element of K6(REAL)
(SVF1 (2,(2,2,f),z0)) /* (h + c) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(SVF1 (2,(2,2,f),z0)) /* c is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
((SVF1 (2,(2,2,f),z0)) /* (h + c)) - ((SVF1 (2,(2,2,f),z0)) /* c) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(h ") (#) (((SVF1 (2,(2,2,f),z0)) /* (h + c)) - ((SVF1 (2,(2,2,f),z0)) /* c)) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim ((h ") (#) (((SVF1 (2,(2,2,f),z0)) /* (h + c)) - ((SVF1 (2,(2,2,f),z0)) /* c))) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is set
partdiff ((2,2,f),z0,2) is V11() real ext-real Element of REAL
diff ((SVF1 (2,(2,2,f),z0)),y0) is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(z0,f) is V11() real ext-real Element of REAL
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,z0) + (1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff (((1,2,z0) + (1,2,f2)),f,1) is V11() real ext-real Element of REAL
(f2,f) is V11() real ext-real Element of REAL
(z0,f) + (f2,f) is V11() real ext-real Element of REAL
partdiff ((1,2,z0),f,1) is V11() real ext-real Element of REAL
partdiff ((1,2,f2),f,1) is V11() real ext-real Element of REAL
(partdiff ((1,2,z0),f,1)) + (partdiff ((1,2,f2),f,1)) is V11() real ext-real Element of REAL
(z0,f) + (partdiff ((1,2,f2),f,1)) is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(z0,f) is V11() real ext-real Element of REAL
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,z0) + (1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff (((1,2,z0) + (1,2,f2)),f,2) is V11() real ext-real Element of REAL
(f2,f) is V11() real ext-real Element of REAL
(z0,f) + (f2,f) is V11() real ext-real Element of REAL
partdiff ((1,2,z0),f,2) is V11() real ext-real Element of REAL
partdiff ((1,2,f2),f,2) is V11() real ext-real Element of REAL
(partdiff ((1,2,z0),f,2)) + (partdiff ((1,2,f2),f,2)) is V11() real ext-real Element of REAL
(z0,f) + (partdiff ((1,2,f2),f,2)) is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(z0,f) is V11() real ext-real Element of REAL
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,z0) + (2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff (((2,2,z0) + (2,2,f2)),f,1) is V11() real ext-real Element of REAL
(f2,f) is V11() real ext-real Element of REAL
(z0,f) + (f2,f) is V11() real ext-real Element of REAL
partdiff ((2,2,z0),f,1) is V11() real ext-real Element of REAL
partdiff ((2,2,f2),f,1) is V11() real ext-real Element of REAL
(partdiff ((2,2,z0),f,1)) + (partdiff ((2,2,f2),f,1)) is V11() real ext-real Element of REAL
(z0,f) + (partdiff ((2,2,f2),f,1)) is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(z0,f) is V11() real ext-real Element of REAL
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,z0) + (2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff (((2,2,z0) + (2,2,f2)),f,2) is V11() real ext-real Element of REAL
(f2,f) is V11() real ext-real Element of REAL
(z0,f) + (f2,f) is V11() real ext-real Element of REAL
partdiff ((2,2,z0),f,2) is V11() real ext-real Element of REAL
partdiff ((2,2,f2),f,2) is V11() real ext-real Element of REAL
(partdiff ((2,2,z0),f,2)) + (partdiff ((2,2,f2),f,2)) is V11() real ext-real Element of REAL
(z0,f) + (partdiff ((2,2,f2),f,2)) is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(z0,f) is V11() real ext-real Element of REAL
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,z0) - (1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff (((1,2,z0) - (1,2,f2)),f,1) is V11() real ext-real Element of REAL
(f2,f) is V11() real ext-real Element of REAL
(z0,f) - (f2,f) is V11() real ext-real Element of REAL
partdiff ((1,2,z0),f,1) is V11() real ext-real Element of REAL
partdiff ((1,2,f2),f,1) is V11() real ext-real Element of REAL
(partdiff ((1,2,z0),f,1)) - (partdiff ((1,2,f2),f,1)) is V11() real ext-real Element of REAL
(z0,f) - (partdiff ((1,2,f2),f,1)) is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(z0,f) is V11() real ext-real Element of REAL
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,z0) - (1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff (((1,2,z0) - (1,2,f2)),f,2) is V11() real ext-real Element of REAL
(f2,f) is V11() real ext-real Element of REAL
(z0,f) - (f2,f) is V11() real ext-real Element of REAL
partdiff ((1,2,z0),f,2) is V11() real ext-real Element of REAL
partdiff ((1,2,f2),f,2) is V11() real ext-real Element of REAL
(partdiff ((1,2,z0),f,2)) - (partdiff ((1,2,f2),f,2)) is V11() real ext-real Element of REAL
(z0,f) - (partdiff ((1,2,f2),f,2)) is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(z0,f) is V11() real ext-real Element of REAL
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,z0) - (2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff (((2,2,z0) - (2,2,f2)),f,1) is V11() real ext-real Element of REAL
(f2,f) is V11() real ext-real Element of REAL
(z0,f) - (f2,f) is V11() real ext-real Element of REAL
partdiff ((2,2,z0),f,1) is V11() real ext-real Element of REAL
partdiff ((2,2,f2),f,1) is V11() real ext-real Element of REAL
(partdiff ((2,2,z0),f,1)) - (partdiff ((2,2,f2),f,1)) is V11() real ext-real Element of REAL
(z0,f) - (partdiff ((2,2,f2),f,1)) is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(z0,f) is V11() real ext-real Element of REAL
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,z0) - (2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff (((2,2,z0) - (2,2,f2)),f,2) is V11() real ext-real Element of REAL
(f2,f) is V11() real ext-real Element of REAL
(z0,f) - (f2,f) is V11() real ext-real Element of REAL
partdiff ((2,2,z0),f,2) is V11() real ext-real Element of REAL
partdiff ((2,2,f2),f,2) is V11() real ext-real Element of REAL
(partdiff ((2,2,z0),f,2)) - (partdiff ((2,2,f2),f,2)) is V11() real ext-real Element of REAL
(z0,f) - (partdiff ((2,2,f2),f,2)) is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
f (#) (1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff ((f (#) (1,2,f2)),z0,1) is V11() real ext-real Element of REAL
(f2,z0) is V11() real ext-real Element of REAL
f * (f2,z0) is V11() real ext-real Element of REAL
partdiff ((1,2,f2),z0,1) is V11() real ext-real Element of REAL
f * (partdiff ((1,2,f2),z0,1)) is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
f (#) (1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff ((f (#) (1,2,f2)),z0,2) is V11() real ext-real Element of REAL
(f2,z0) is V11() real ext-real Element of REAL
f * (f2,z0) is V11() real ext-real Element of REAL
partdiff ((1,2,f2),z0,2) is V11() real ext-real Element of REAL
f * (partdiff ((1,2,f2),z0,2)) is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
f (#) (2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff ((f (#) (2,2,f2)),z0,1) is V11() real ext-real Element of REAL
(f2,z0) is V11() real ext-real Element of REAL
f * (f2,z0) is V11() real ext-real Element of REAL
partdiff ((2,2,f2),z0,1) is V11() real ext-real Element of REAL
f * (partdiff ((2,2,f2),z0,1)) is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
f (#) (2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
partdiff ((f (#) (2,2,f2)),z0,2) is V11() real ext-real Element of REAL
(f2,z0) is V11() real ext-real Element of REAL
f * (f2,z0) is V11() real ext-real Element of REAL
partdiff ((2,2,f2),z0,2) is V11() real ext-real Element of REAL
f * (partdiff ((2,2,f2),z0,2)) is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,z0) (#) (1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,z0) (#) (1,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,z0) (#) (2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
f is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
z0 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,z0) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
f2 is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,z0) (#) (2,2,f2) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,f) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
SVF1 (1,(1,2,f),z0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (1,2)) . z0 is V11() real ext-real Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(1,2,f) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
SVF1 (2,(1,2,f),z0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (2,2)) . z0 is V11() real ext-real Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,f) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
SVF1 (1,(2,2,f),z0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (1,2)) . z0 is V11() real ext-real Element of REAL
f is V16() V19( REAL 2) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
(2,2,f) is non empty V16() V19( REAL 2) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))
z0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(2) FinSequence-like Element of REAL 2
SVF1 (2,(2,2,f),z0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (2,2)) . z0 is V11() real ext-real Element of REAL