:: PDIFF_5 semantic presentation

REAL is V1() 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 V1() V54() V160() V166() set

RAT is V1() V54() V160() V161() V162() V163() V166() set

INT is V1() V54() V160() V161() V162() V163() V164() V166() set

1 is V1() 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 V1() 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 V1() 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 V1() 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 ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

the V1() V160() V161() V162() V163() V164() V165() V166() set is V1() V160() V161() V162() V163() V164() V165() V166() set

3 is V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

0 is set

REAL 3 is V1() FinSequence-membered M11( REAL )

K7((REAL 3),REAL) is complex-valued ext-real-valued real-valued set

K6(K7((REAL 3),REAL)) is set

proj (1,3) is V1() V16() V19( REAL 3) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))

proj (2,3) is V1() V16() V19( REAL 3) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))

proj (3,3) is V1() V16() V19( REAL 3) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))

f is V16() V19( REAL 3) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))

u0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(3) FinSequence-like Element of REAL 3

pdiff1 (f,1) is V1() V16() V19( REAL 3) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))

SVF1 (1,(pdiff1 (f,1)),u0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom (SVF1 (1,(pdiff1 (f,1)),u0)) 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

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

<*f2,h,c*> is set

(SVF1 (1,(pdiff1 (f,1)),u0)) . f2 is V11() real ext-real Element of REAL

x0 is V160() V161() V162() Neighbourhood of f2

y0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z0 is V1() 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 V160() V161() V162() Neighbourhood of f2

y0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z0 is V1() 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 V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z0 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z1 is V11() real ext-real Element of REAL

y0 . 1 is V11() real ext-real Element of REAL

z1 * 1 is V11() real ext-real Element of REAL

N is V160() V161() V162() Neighbourhood of f2

L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

R is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

N1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,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

y0 is V11() real ext-real Element of REAL

<*c,x0,y0*> is set

z0 is V160() V161() V162() Neighbourhood of c

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

(SVF1 (1,(pdiff1 (f,1)),u0)) . c is V11() real ext-real Element of REAL

N is V1() 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

y0 is V11() real ext-real Element of REAL

<*c,x0,y0*> is set

(SVF1 (1,(pdiff1 (f,1)),u0)) . c is V11() real ext-real Element of REAL

z0 is V160() V161() V162() Neighbourhood of c

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

N is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z0 is V160() V161() V162() Neighbourhood of c

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

N is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

N is V1() 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 V11() real ext-real Element of REAL

R is V11() real ext-real Element of REAL

z1 is V11() real ext-real Element of REAL

<*L,R,z1*> is set

N1 is V160() V161() V162() Neighbourhood of L

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

(SVF1 (1,(pdiff1 (f,1)),u0)) . L is V11() real ext-real Element of REAL

R1 is V1() 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 V11() real ext-real Element of REAL

R is V11() real ext-real Element of REAL

z1 is V11() real ext-real Element of REAL

<*L,R,z1*> is set

(SVF1 (1,(pdiff1 (f,1)),u0)) . L is V11() real ext-real Element of REAL

N1 is V160() V161() V162() Neighbourhood of L

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

R1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

N1 is V160() V161() V162() Neighbourhood of L

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

R1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

R1 is V1() 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

p1 is V11() real ext-real Element of REAL

r1 * 1 is V11() real ext-real Element of REAL

p1 * 1 is V11() real ext-real Element of REAL

N0 is V160() V161() V162() Neighbourhood of c

g is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

g . 1 is V11() real ext-real Element of REAL

s1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

h is V160() V161() V162() Neighbourhood of L

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

c

N0 is V11() real ext-real Element of REAL

(SVF1 (1,(pdiff1 (f,1)),u0)) . N0 is V11() real ext-real Element of REAL

((SVF1 (1,(pdiff1 (f,1)),u0)) . N0) - ((SVF1 (1,(pdiff1 (f,1)),u0)) . c) is V11() real ext-real Element of REAL

N0 - c is V11() real ext-real Element of REAL

z1 . (N0 - c) is V11() real ext-real Element of REAL

N . (N0 - c) is V11() real ext-real Element of REAL

(z1 . (N0 - c)) + (N . (N0 - c)) is V11() real ext-real Element of REAL

L1 . (N0 - c) is V11() real ext-real Element of REAL

R1 . (N0 - c) is V11() real ext-real Element of REAL

(L1 . (N0 - c)) + (R1 . (N0 - c)) is V11() real ext-real Element of REAL

r1 * (N0 - c) is V11() real ext-real Element of REAL

(r1 * (N0 - c)) + (N . (N0 - c)) is V11() real ext-real Element of REAL

f2 * (N0 - c) is V11() real ext-real Element of REAL

(f2 * (N0 - c)) + (N . (N0 - c)) is V11() real ext-real Element of REAL

h * (N0 - c) is V11() real ext-real Element of REAL

(h * (N0 - c)) + (R1 . (N0 - c)) is V11() real ext-real Element of REAL

N0 is V160() V161() V162() Neighbourhood of c

g is V11() real ext-real set

c - g is V11() real ext-real Element of REAL

c + g is V11() real ext-real Element of REAL

].(c - g),(c + g).[ is V160() V161() V162() Element of K6(REAL)

{ b

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 V1() 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 V1() ordinal natural V11() real ext-real positive non negative Element of REAL

g / (n + 2) is V11() real ext-real Element of REAL

n + 1 is V1() ordinal natural V11() real ext-real positive non negative Element of REAL

(n + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative Element of REAL

0 + 1 is V1() ordinal natural V11() real ext-real positive non negative Element of REAL

g / 1 is V11() real ext-real Element of REAL

c + (g / (n + 2)) is V11() real ext-real Element of REAL

- g is V11() real ext-real set

c + (- g) is V11() real ext-real Element of REAL

(c + (g / (n + 2))) - c 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))

R1 /* 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 ") (#) (R1 /* h) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

N /* 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 /* 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 ") (#) (R1 /* h)) - ((h ") (#) (N /* h)) is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

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

(((h ") (#) (R1 /* h)) - ((h ") (#) (N /* h))) . n is V11() real ext-real Element of REAL

h . n is V11() real ext-real Element of REAL

f2 * (h . n) is V11() real ext-real Element of REAL

N . (h . n) is V11() real ext-real Element of REAL

(f2 * (h . n)) + (N . (h . n)) is V11() real ext-real Element of REAL

h * (h . n) is V11() real ext-real Element of REAL

R1 . (h . n) is V11() real ext-real Element of REAL

(h * (h . n)) + (R1 . (h . n)) is V11() real ext-real Element of REAL

c

c

(f2 * (h . n)) / (h . n) is V11() real ext-real Element of REAL

(N . (h . n)) / (h . n) is V11() real ext-real Element of REAL

((f2 * (h . n)) / (h . n)) + ((N . (h . n)) / (h . n)) is V11() real ext-real Element of REAL

((h * (h . n)) + (R1 . (h . n))) / (h . n) is V11() real ext-real Element of REAL

(h . n) / (h . n) 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

(h * (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 + ((N . (h . n)) / (h . n)) is V11() real ext-real Element of REAL

(R1 . (h . n)) / (h . n) is V11() real ext-real Element of REAL

h + ((R1 . (h . n)) / (h . n)) is V11() real ext-real Element of REAL

dom N is V160() V161() V162() Element of K6(REAL)

rng h is V160() V161() V162() Element of K6(REAL)

dom R1 is V160() V161() V162() Element of K6(REAL)

(h . n) " is V11() real ext-real Element of REAL

(N . (h . n)) * ((h . n) ") is V11() real ext-real Element of REAL

(h ") . n is V11() real ext-real Element of REAL

(N . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL

(N /* h) . n is V11() real ext-real Element of REAL

((N /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL

((h ") (#) (N /* h)) . n is V11() real ext-real Element of REAL

(R1 . (h . n)) * ((h . n) ") is V11() real ext-real Element of REAL

(R1 . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL

(R1 /* h) . n is V11() real ext-real Element of REAL

((R1 /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL

((h ") (#) (R1 /* h)) . n is V11() real ext-real Element of REAL

(((h ") (#) (R1 /* h)) . n) - (((h ") (#) (N /* h)) . n) is V11() real ext-real Element of REAL

h + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (N /* h)) . n)) is V11() real ext-real Element of REAL

(((h ") (#) (R1 /* h)) - ((h ") (#) (N /* h))) . 1 is V11() real ext-real Element of REAL

lim (((h ") (#) (R1 /* h)) - ((h ") (#) (N /* h))) is V11() real ext-real Element of REAL

lim ((h ") (#) (N /* h)) is V11() real ext-real Element of REAL

lim ((h ") (#) (R1 /* h)) is V11() real ext-real Element of REAL

0 - 0 is V11() real ext-real Element of REAL

f is V16() V19( REAL 3) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))

u0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(3) FinSequence-like Element of REAL 3

pdiff1 (f,1) is V1() V16() V19( REAL 3) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))

SVF1 (2,(pdiff1 (f,1)),u0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom (SVF1 (2,(pdiff1 (f,1)),u0)) 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

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

<*f2,h,c*> is set

(SVF1 (2,(pdiff1 (f,1)),u0)) . h is V11() real ext-real Element of REAL

x0 is V160() V161() V162() Neighbourhood of h

y0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z0 is V1() 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 V160() V161() V162() Neighbourhood of h

y0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z0 is V1() 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 V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z0 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z1 is V11() real ext-real Element of REAL

y0 . 1 is V11() real ext-real Element of REAL

z1 * 1 is V11() real ext-real Element of REAL

N is V160() V161() V162() Neighbourhood of h

L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

R is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

N1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,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

y0 is V11() real ext-real Element of REAL

<*c,x0,y0*> is set

z0 is V160() V161() V162() Neighbourhood of x0

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

(SVF1 (2,(pdiff1 (f,1)),u0)) . x0 is V11() real ext-real Element of REAL

N is V1() 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

y0 is V11() real ext-real Element of REAL

<*c,x0,y0*> is set

(SVF1 (2,(pdiff1 (f,1)),u0)) . x0 is V11() real ext-real Element of REAL

z0 is V160() V161() V162() Neighbourhood of x0

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

N is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z0 is V160() V161() V162() Neighbourhood of x0

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

N is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

N is V1() 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

L is V11() real ext-real Element of REAL

z1 is V11() real ext-real Element of REAL

<*L,R,z1*> is set

N1 is V160() V161() V162() Neighbourhood of R

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

(SVF1 (2,(pdiff1 (f,1)),u0)) . R is V11() real ext-real Element of REAL

R1 is V1() 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 V11() real ext-real Element of REAL

R is V11() real ext-real Element of REAL

z1 is V11() real ext-real Element of REAL

<*L,R,z1*> is set

(SVF1 (2,(pdiff1 (f,1)),u0)) . R is V11() real ext-real Element of REAL

N1 is V160() V161() V162() Neighbourhood of R

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

R1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

N1 is V160() V161() V162() Neighbourhood of R

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

R1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

R1 is V1() 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

p1 is V11() real ext-real Element of REAL

r1 * 1 is V11() real ext-real Element of REAL

p1 * 1 is V11() real ext-real Element of REAL

N0 is V160() V161() V162() Neighbourhood of x0

g is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

g . 1 is V11() real ext-real Element of REAL

s1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

h is V160() V161() V162() Neighbourhood of R

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

c

N0 is V11() real ext-real Element of REAL

(SVF1 (2,(pdiff1 (f,1)),u0)) . N0 is V11() real ext-real Element of REAL

((SVF1 (2,(pdiff1 (f,1)),u0)) . N0) - ((SVF1 (2,(pdiff1 (f,1)),u0)) . x0) is V11() real ext-real Element of REAL

N0 - x0 is V11() real ext-real Element of REAL

z1 . (N0 - x0) is V11() real ext-real Element of REAL

N . (N0 - x0) is V11() real ext-real Element of REAL

(z1 . (N0 - x0)) + (N . (N0 - x0)) is V11() real ext-real Element of REAL

L1 . (N0 - x0) is V11() real ext-real Element of REAL

R1 . (N0 - x0) is V11() real ext-real Element of REAL

(L1 . (N0 - x0)) + (R1 . (N0 - x0)) is V11() real ext-real Element of REAL

r1 * (N0 - x0) is V11() real ext-real Element of REAL

(r1 * (N0 - x0)) + (N . (N0 - x0)) is V11() real ext-real Element of REAL

f2 * (N0 - x0) is V11() real ext-real Element of REAL

(f2 * (N0 - x0)) + (N . (N0 - x0)) is V11() real ext-real Element of REAL

h * (N0 - x0) is V11() real ext-real Element of REAL

(h * (N0 - x0)) + (R1 . (N0 - x0)) 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)

{ b

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 V1() 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 V1() ordinal natural V11() real ext-real positive non negative Element of REAL

g / (n + 2) is V11() real ext-real Element of REAL

n + 1 is V1() ordinal natural V11() real ext-real positive non negative Element of REAL

(n + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative Element of REAL

0 + 1 is V1() ordinal natural V11() real ext-real positive non negative Element of REAL

g / 1 is V11() real ext-real Element of REAL

x0 + (g / (n + 2)) 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

(x0 + (g / (n + 2))) - x0 is V11() real ext-real Element of 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

N . (h . n) is V11() real ext-real Element of REAL

(f2 * (h . n)) + (N . (h . n)) is V11() real ext-real Element of REAL

h * (h . n) is V11() real ext-real Element of REAL

R1 . (h . n) is V11() real ext-real Element of REAL

(h * (h . n)) + (R1 . (h . n)) is V11() real ext-real Element of REAL

c

c

(f2 * (h . n)) / (h . n) is V11() real ext-real Element of REAL

(N . (h . n)) / (h . n) is V11() real ext-real Element of REAL

((f2 * (h . n)) / (h . n)) + ((N . (h . n)) / (h . n)) is V11() real ext-real Element of REAL

((h * (h . n)) + (R1 . (h . n))) / (h . n) is V11() real ext-real Element of REAL

(h . n) / (h . n) 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

(h * (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 + ((N . (h . n)) / (h . n)) is V11() real ext-real Element of REAL

(R1 . (h . n)) / (h . n) is V11() real ext-real Element of REAL

h + ((R1 . (h . n)) / (h . n)) is V11() real ext-real Element of REAL

dom N is V160() V161() V162() Element of K6(REAL)

rng h is V160() V161() V162() Element of K6(REAL)

dom R1 is V160() V161() V162() Element of K6(REAL)

(h . n) " is V11() real ext-real Element of REAL

(N . (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

(N . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL

N /* h is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(N /* h) . n is V11() real ext-real Element of REAL

((N /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL

(h ") (#) (N /* 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 /* h)) . n is V11() real ext-real Element of REAL

(R1 . (h . n)) * ((h . n) ") is V11() real ext-real Element of REAL

(R1 . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL

R1 /* h is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(R1 /* h) . n is V11() real ext-real Element of REAL

((R1 /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL

(h ") (#) (R1 /* 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 ") (#) (R1 /* h)) . n is V11() real ext-real Element of REAL

(((h ") (#) (R1 /* h)) . n) - (((h ") (#) (N /* h)) . n) is V11() real ext-real Element of REAL

h + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (N /* h)) . n)) is V11() real ext-real Element of REAL

f2 - h is V11() real ext-real Element of REAL

((h ") (#) (R1 /* h)) - ((h ") (#) (N /* 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 ") (#) (R1 /* h)) - ((h ") (#) (N /* h))) . n is V11() real ext-real Element of REAL

(((h ") (#) (R1 /* h)) - ((h ") (#) (N /* h))) . 1 is V11() real ext-real Element of REAL

lim (((h ") (#) (R1 /* h)) - ((h ") (#) (N /* h))) is V11() real ext-real Element of REAL

lim ((h ") (#) (N /* h)) is V11() real ext-real Element of REAL

lim ((h ") (#) (R1 /* h)) is V11() real ext-real Element of REAL

0 - 0 is V11() real ext-real Element of REAL

f is V16() V19( REAL 3) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))

u0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(3) FinSequence-like Element of REAL 3

pdiff1 (f,1) is V1() V16() V19( REAL 3) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))

SVF1 (3,(pdiff1 (f,1)),u0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom (SVF1 (3,(pdiff1 (f,1)),u0)) 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

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

<*f2,h,c*> is set

(SVF1 (3,(pdiff1 (f,1)),u0)) . c is V11() real ext-real Element of REAL

x0 is V160() V161() V162() Neighbourhood of c

y0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z0 is V1() 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 V160() V161() V162() Neighbourhood of c

y0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z0 is V1() 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 V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z0 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z1 is V11() real ext-real Element of REAL

y0 . 1 is V11() real ext-real Element of REAL

z1 * 1 is V11() real ext-real Element of REAL

N is V160() V161() V162() Neighbourhood of c

L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

R is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

N1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

f2 is V11() real ext-real Element of REAL

h is V11() real ext-real Element of REAL

y0 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,y0*> is set

z0 is V160() V161() V162() Neighbourhood of y0

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

(SVF1 (3,(pdiff1 (f,1)),u0)) . y0 is V11() real ext-real Element of REAL

N is V1() 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

y0 is V11() real ext-real Element of REAL

<*c,x0,y0*> is set

(SVF1 (3,(pdiff1 (f,1)),u0)) . y0 is V11() real ext-real Element of REAL

z0 is V160() V161() V162() Neighbourhood of y0

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

N is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z0 is V160() V161() V162() Neighbourhood of y0

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

N is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

N is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z1 is V11() real ext-real Element of REAL

L is V11() real ext-real Element of REAL

R is V11() real ext-real Element of REAL

<*L,R,z1*> is set

N1 is V160() V161() V162() Neighbourhood of z1

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

(SVF1 (3,(pdiff1 (f,1)),u0)) . z1 is V11() real ext-real Element of REAL

R1 is V1() 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 V11() real ext-real Element of REAL

R is V11() real ext-real Element of REAL

z1 is V11() real ext-real Element of REAL

<*L,R,z1*> is set

(SVF1 (3,(pdiff1 (f,1)),u0)) . z1 is V11() real ext-real Element of REAL

N1 is V160() V161() V162() Neighbourhood of z1

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

R1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

N1 is V160() V161() V162() Neighbourhood of z1

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

R1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

R1 is V1() 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

p1 is V11() real ext-real Element of REAL

r1 * 1 is V11() real ext-real Element of REAL

p1 * 1 is V11() real ext-real Element of REAL

N0 is V160() V161() V162() Neighbourhood of y0

g is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

g . 1 is V11() real ext-real Element of REAL

s1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

h is V160() V161() V162() Neighbourhood of z1

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

c

N0 is V11() real ext-real Element of REAL

(SVF1 (3,(pdiff1 (f,1)),u0)) . N0 is V11() real ext-real Element of REAL

((SVF1 (3,(pdiff1 (f,1)),u0)) . N0) - ((SVF1 (3,(pdiff1 (f,1)),u0)) . y0) is V11() real ext-real Element of REAL

N0 - y0 is V11() real ext-real Element of REAL

z1 . (N0 - y0) is V11() real ext-real Element of REAL

N . (N0 - y0) is V11() real ext-real Element of REAL

(z1 . (N0 - y0)) + (N . (N0 - y0)) is V11() real ext-real Element of REAL

L1 . (N0 - y0) is V11() real ext-real Element of REAL

R1 . (N0 - y0) is V11() real ext-real Element of REAL

(L1 . (N0 - y0)) + (R1 . (N0 - y0)) is V11() real ext-real Element of REAL

r1 * (N0 - y0) is V11() real ext-real Element of REAL

(r1 * (N0 - y0)) + (N . (N0 - y0)) is V11() real ext-real Element of REAL

f2 * (N0 - y0) is V11() real ext-real Element of REAL

(f2 * (N0 - y0)) + (N . (N0 - y0)) is V11() real ext-real Element of REAL

h * (N0 - y0) is V11() real ext-real Element of REAL

(h * (N0 - y0)) + (R1 . (N0 - y0)) 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)

{ b

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 V1() 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 V1() ordinal natural V11() real ext-real positive non negative Element of REAL

g / (n + 2) is V11() real ext-real Element of REAL

n + 1 is V1() ordinal natural V11() real ext-real positive non negative Element of REAL

(n + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative Element of REAL

0 + 1 is V1() ordinal natural V11() real ext-real positive non negative Element of REAL

g / 1 is V11() real ext-real Element of REAL

y0 + (g / (n + 2)) 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

(y0 + (g / (n + 2))) - y0 is V11() real ext-real Element of 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

N . (h . n) is V11() real ext-real Element of REAL

(f2 * (h . n)) + (N . (h . n)) is V11() real ext-real Element of REAL

h * (h . n) is V11() real ext-real Element of REAL

R1 . (h . n) is V11() real ext-real Element of REAL

(h * (h . n)) + (R1 . (h . n)) is V11() real ext-real Element of REAL

c

c

(f2 * (h . n)) / (h . n) is V11() real ext-real Element of REAL

(N . (h . n)) / (h . n) is V11() real ext-real Element of REAL

((f2 * (h . n)) / (h . n)) + ((N . (h . n)) / (h . n)) is V11() real ext-real Element of REAL

((h * (h . n)) + (R1 . (h . n))) / (h . n) is V11() real ext-real Element of REAL

(h . n) / (h . n) 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

(h * (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 + ((N . (h . n)) / (h . n)) is V11() real ext-real Element of REAL

(R1 . (h . n)) / (h . n) is V11() real ext-real Element of REAL

h + ((R1 . (h . n)) / (h . n)) is V11() real ext-real Element of REAL

dom N is V160() V161() V162() Element of K6(REAL)

rng h is V160() V161() V162() Element of K6(REAL)

dom R1 is V160() V161() V162() Element of K6(REAL)

(h . n) " is V11() real ext-real Element of REAL

(N . (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

(N . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL

N /* h is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(N /* h) . n is V11() real ext-real Element of REAL

((N /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL

(h ") (#) (N /* 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 /* h)) . n is V11() real ext-real Element of REAL

(R1 . (h . n)) * ((h . n) ") is V11() real ext-real Element of REAL

(R1 . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL

R1 /* h is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(R1 /* h) . n is V11() real ext-real Element of REAL

((R1 /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL

(h ") (#) (R1 /* 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 ") (#) (R1 /* h)) . n is V11() real ext-real Element of REAL

(((h ") (#) (R1 /* h)) . n) - (((h ") (#) (N /* h)) . n) is V11() real ext-real Element of REAL

h + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (N /* h)) . n)) is V11() real ext-real Element of REAL

f2 - h is V11() real ext-real Element of REAL

((h ") (#) (R1 /* h)) - ((h ") (#) (N /* 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 ") (#) (R1 /* h)) - ((h ") (#) (N /* h))) . n is V11() real ext-real Element of REAL

(((h ") (#) (R1 /* h)) - ((h ") (#) (N /* h))) . 1 is V11() real ext-real Element of REAL

lim (((h ") (#) (R1 /* h)) - ((h ") (#) (N /* h))) is V11() real ext-real Element of REAL

lim ((h ") (#) (N /* h)) is V11() real ext-real Element of REAL

lim ((h ") (#) (R1 /* h)) is V11() real ext-real Element of REAL

0 - 0 is V11() real ext-real Element of REAL

f is V16() V19( REAL 3) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))

u0 is V16() V19( NAT ) V20( REAL ) V21() complex-valued ext-real-valued real-valued V61(3) FinSequence-like Element of REAL 3

pdiff1 (f,2) is V1() V16() V19( REAL 3) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 3),REAL))

SVF1 (1,(pdiff1 (f,2)),u0) is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom (SVF1 (1,(pdiff1 (f,2)),u0)) 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

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

<*f2,h,c*> is set

(SVF1 (1,(pdiff1 (f,2)),u0)) . f2 is V11() real ext-real Element of REAL

x0 is V160() V161() V162() Neighbourhood of f2

y0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z0 is V1() 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 V160() V161() V162() Neighbourhood of f2

y0 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z0 is V1() 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 V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z0 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z1 is V11() real ext-real Element of REAL

y0 . 1 is V11() real ext-real Element of REAL

z1 * 1 is V11() real ext-real Element of REAL

N is V160() V161() V162() Neighbourhood of f2

L is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

R is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

N1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,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

y0 is V11() real ext-real Element of REAL

<*c,x0,y0*> is set

z0 is V160() V161() V162() Neighbourhood of c

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

(SVF1 (1,(pdiff1 (f,2)),u0)) . c is V11() real ext-real Element of REAL

N is V1() 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

y0 is V11() real ext-real Element of REAL

<*c,x0,y0*> is set

(SVF1 (1,(pdiff1 (f,2)),u0)) . c is V11() real ext-real Element of REAL

z0 is V160() V161() V162() Neighbourhood of c

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

N is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z0 is V160() V161() V162() Neighbourhood of c

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

N is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

z1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

z1 . 1 is V11() real ext-real Element of REAL

N is V1() 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 V11() real ext-real Element of REAL

R is V11() real ext-real Element of REAL

z1 is V11() real ext-real Element of REAL

<*L,R,z1*> is set

N1 is V160() V161() V162() Neighbourhood of L

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

(SVF1 (1,(pdiff1 (f,2)),u0)) . L is V11() real ext-real Element of REAL

R1 is V1() 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 V11() real ext-real Element of REAL

R is V11() real ext-real Element of REAL

z1 is V11() real ext-real Element of REAL

<*L,R,z1*> is set

(SVF1 (1,(pdiff1 (f,2)),u0)) . L is V11() real ext-real Element of REAL

N1 is V160() V161() V162() Neighbourhood of L

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

R1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

N1 is V160() V161() V162() Neighbourhood of L

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

R1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

L1 is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 . 1 is V11() real ext-real Element of REAL

R1 is V1() 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

p1 is V11() real ext-real Element of REAL

r1 * 1 is V11() real ext-real Element of REAL

p1 * 1 is V11() real ext-real Element of REAL

N0 is V160() V161() V162() Neighbourhood of c

g is V16() V19( REAL ) V20( REAL ) V21() complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

g . 1 is V11() real ext-real Element of REAL

s1 is V1() V16() V19( REAL ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

h is V160() V161() V162() Neighbourhood of L

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

c

N0 is V11() real ext-real Element of REAL

(SVF1 (1,(pdiff1 (f,2)),u0)) . N0 is V11() real ext-real Element of REAL

((SVF1 (1,(pdiff1 (f,2)),u0)) . N0) - ((SVF1 (1,(pdiff1 (f,2)),u0)) . c) is V11() real ext-real Element of REAL

N0 - c is V11() real ext-real Element of REAL

z1 . (N0 - c) is V11() real ext-real Element of REAL

N . (N0 - c) is V11() real ext-real Element of REAL

(z1 . (N0 - c)) + (N . (N0 - c)) is V11() real ext-real Element of REAL

L1 . (N0 - c) is V11() real ext-real Element of REAL

R1 . (N0 - c) is V11() real ext-real Element of REAL

(L1 . (N0 - c)) + (R1 . (N0 - c)) is V11() real ext-real Element of REAL

r1 * (N0 - c) is V11() real ext-real Element of REAL

(r1 * (N0 - c)) + (N . (N0 - c)) is V11() real ext-real Element of REAL

f2 * (N0 - c) is V11() real ext-real Element of REAL

(f2 * (N0 - c)) + (N . (N0 - c)) is V11() real ext-real Element of REAL

h * (N0 - c) is V11() real ext-real Element of REAL

(h * (N0 - c)) + (R1 . (N0 - c)) is V11() real ext-real Element of REAL

N0 is V160() V161() V162() Neighbourhood of c

g is V11() real ext-real set

c - g is V11() real ext-real Element of REAL

c + g is V11() real ext-real Element of REAL

].(c - g),(c + g).[ is V160() V161() V162() Element of K6(REAL)

{ b

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 V1() 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 V1() ordinal natural V11() real ext-real positive non negative Element of REAL

g / (n + 2) is V11() real ext-real Element of REAL

n + 1 is V1() ordinal natural V11() real ext-real positive non negative Element of REAL

(n + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative Element of REAL

0 + 1 is V1() ordinal natural V11() real ext-real positive non negative Element of REAL

g / 1 is V11() real ext-real Element of REAL

c + (g / (n + 2)) is V11() real ext-real Element of REAL

- g is V11() real ext-real set

c + (- g) is V11() real ext-real Element of REAL

(c + (g / (n + 2))) - c is V11() real ext-real Element of 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

N . (h . n) is V11() real ext-real Element of REAL

(f2 * (h . n)) + (N . (h . n)) is V11() real ext-real Element of REAL

h * (h . n) is V11() real ext-real Element of REAL

R1 . (h . n) is V11() real ext-real Element of REAL

(h * (h . n)) + (R1 . (h . n)) is V11() real ext-real Element of REAL

c

c

(f2 * (h . n)) / (h . n) is V11() real ext-real Element of REAL

(N . (h . n)) / (h . n) is V11() real ext-real Element of REAL

((f2 * (h . n)) / (h . n)) + ((N . (h . n)) / (h . n)) is V11() real ext-real Element of REAL

((h * (h . n)) + (R1 . (h . n))) / (h . n) is V11() real ext-real Element of REAL

(h . n) / (h . n) 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

(h * (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 + ((N . (h . n)) / (h . n)) is V11() real ext-real Element of REAL

(R1 . (h . n)) / (h . n) is V11() real ext-real Element of REAL

h + ((R1 . (h . n)) / (h . n)) is V11() real ext-real Element of REAL

dom N is V160() V161() V162() Element of K6(REAL)

rng h is V160() V161() V162() Element of K6(REAL)

dom R1 is V160() V161() V162() Element of K6(REAL)

(h . n) " is V11() real ext-real Element of REAL

(N . (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

(N . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL

N /* h is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(N /* h) . n is V11() real ext-real Element of REAL

((N /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL

(h ") (#) (N /* 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 /* h)) . n is V11() real ext-real Element of REAL

(R1 . (h . n)) * ((h . n) ") is V11() real ext-real Element of REAL

(R1 . (h . n)) * ((h ") . n) is V11() real ext-real Element of REAL

R1 /* h is V16() V19( NAT ) V20( REAL ) V21() total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(R1 /* h) . n is V11() real ext-real Element of REAL

((R1 /* h) . n) * ((h ") . n) is V11() real ext-real Element of REAL

(h ") (#) (R1 /* 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 ") (#) (R1 /* h)) . n is V11() real ext-real Element of REAL

(((h ") (#) (R1 /* h)) . n) - (((h ") (#) (N /* h)) . n) is V11() real ext-real Element of REAL

h + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (N /* h)) . n)) is V11() real