:: PDIFF_2 semantic presentation

REAL is V1() V54() V160() V161() V162() V166() set

NAT is V1() epsilon-transitive epsilon-connected ordinal V160() V161() V162() V163() V164() V165() V166() Element of K6(REAL)

K6(REAL) is set

COMPLEX is V1() V54() V160() V166() set

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

K6(K7(REAL,REAL)) is set

omega is V1() epsilon-transitive epsilon-connected ordinal 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

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

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

1 is V1() epsilon-transitive epsilon-connected 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() epsilon-transitive epsilon-connected 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

K407(2) is V66() V92() V117() V118() V119() V120() V121() V122() V123() V172() V202() L20()

the U1 of K407(2) is set

REAL 1 is V1() functional FinSequence-membered FinSequenceSet of REAL

1 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

K7((REAL 1),(REAL 1)) is set

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

K418(1) is V66() V129() L15()

the U1 of K418(1) is set

K279(K418(1),K418(1)) is V66() L15()

the U1 of K279(K418(1),K418(1)) 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 V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional FinSequence-membered V136() V159() V160() V161() V162() V163() V164() V165() V166() Element of NAT

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

0c is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional FinSequence-membered V160() V161() V162() V163() V164() V165() V166() set

REAL 2 is V1() functional FinSequence-membered FinSequenceSet of REAL

2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

K6((REAL 2)) is set

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

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

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

dom (proj (1,2)) is functional FinSequence-membered Element of K6((REAL 2))

rng (proj (1,2)) is V160() V161() V162() Element of K6(REAL)

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

x0 is set

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

<*y0, the V11() real ext-real Element of REAL *> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

y0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

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

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

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

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

<*z0,x0*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

(proj (1,2)) . <*z0,x0*> is V11() real ext-real Element of REAL

<*z0,x0*> . 1 is set

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

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

<*z0,x0*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

(proj (1,2)) . <*z0,x0*> is V11() real ext-real Element of REAL

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

dom (proj (2,2)) is functional FinSequence-membered Element of K6((REAL 2))

rng (proj (2,2)) is V160() V161() V162() Element of K6(REAL)

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

x0 is set

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

<* the V11() real ext-real Element of REAL ,y0*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

y0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

(proj (2,2)) . y0 is V11() real ext-real Element of REAL

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

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

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

<*z0,x0*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

(proj (2,2)) . <*z0,x0*> is V11() real ext-real Element of REAL

<*z0,x0*> . 2 is set

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

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

<*z0,x0*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

(proj (2,2)) . <*z0,x0*> is V11() real ext-real Element of REAL

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

REAL f is V1() functional FinSequence-membered FinSequenceSet of REAL

f -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL

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

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

z0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

y0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(f) FinSequence-like FinSubsequence-like Element of REAL f

reproj (z0,y0) is V1() V16() V19( REAL ) V20( REAL f) Function-like total quasi_total Element of K6(K7(REAL,(REAL f)))

K7(REAL,(REAL f)) is set

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

x0 is V16() V19( REAL f) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL f),REAL))

x0 * (reproj (z0,y0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

x0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

y0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

(2,1,y0,x0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

reproj (1,x0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

y0 * (reproj (1,x0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

(proj (1,2)) . x0 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

x0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

y0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

(2,2,y0,x0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

reproj (2,x0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

y0 * (reproj (2,x0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

(proj (2,2)) . x0 is V11() real ext-real Element of REAL

f is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

z0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

(2,1,f,z0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

reproj (1,z0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

f * (reproj (1,z0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

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

<*y0,N1*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

(proj (1,2)) . z0 is V11() real ext-real Element of REAL

f is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

z0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

(2,2,f,z0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

reproj (2,z0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

f * (reproj (2,z0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

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

<*y0,N1*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

(proj (2,2)) . z0 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

x0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

y0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

(2,1,y0,x0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

reproj (1,x0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

y0 * (reproj (1,x0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom (2,1,y0,x0) is V160() V161() V162() Element of K6(REAL)

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

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

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

<*y0,N1*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

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

<*f,z0*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

x0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

y0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

(2,2,y0,x0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

reproj (2,x0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

y0 * (reproj (2,x0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom (2,2,y0,x0) is V160() V161() V162() Element of K6(REAL)

(2,2,y0,x0) . z0 is V11() real ext-real Element of REAL

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

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

<*y0,N1*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

f is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

z0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

(2,1,f,z0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

reproj (1,z0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

f * (reproj (1,z0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom (2,1,f,z0) 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

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

N1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 is V16() V19( REAL ) V20( REAL ) Function-like 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

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

N1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 is V16() V19( REAL ) V20( REAL ) Function-like 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

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

N1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

f is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

z0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

(2,2,f,z0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

reproj (2,z0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

f * (reproj (2,z0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom (2,2,f,z0) 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

(2,2,f,z0) . y0 is V11() real ext-real Element of REAL

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

N1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

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

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

<*x0,y0*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

(2,2,f,z0) . y0 is V11() real ext-real Element of REAL

N1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 is V16() V19( REAL ) V20( REAL ) Function-like 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

(2,2,f,z0) . y0 is V11() real ext-real Element of REAL

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

N1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

L1 is V16() V19( REAL ) V20( REAL ) Function-like 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

y0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

y0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

(2,1,y0,y0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

reproj (1,y0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

y0 * (reproj (1,y0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

diff ((2,1,y0,y0),f) is V11() real ext-real Element of REAL

dom (2,1,y0,y0) is V160() V161() V162() Element of K6(REAL)

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

L1 is V160() V161() V162() Neighbourhood of f

R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

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

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

<*L1,R1*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

x1 is V160() V161() V162() Neighbourhood of L1

y1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

N2 is V16() V19( REAL ) V20( REAL ) Function-like 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

y0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

y0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

(2,2,y0,y0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

reproj (2,y0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

y0 * (reproj (2,y0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

diff ((2,2,y0,y0),z0) is V11() real ext-real Element of REAL

dom (2,2,y0,y0) is V160() V161() V162() Element of K6(REAL)

(2,2,y0,y0) . z0 is V11() real ext-real Element of REAL

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

R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

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

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

<*L1,R1*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

x1 is V160() V161() V162() Neighbourhood of R1

y1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

N2 is V16() V19( REAL ) V20( REAL ) Function-like 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

y0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

y0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

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

reproj (1,y0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

y0 * (reproj (1,y0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

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

diff ((y0 * (reproj (1,y0))),((proj (1,2)) . y0)) is V11() real ext-real Element of REAL

(2,1,y0,y0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom (2,1,y0,y0) is V160() V161() V162() Element of K6(REAL)

diff ((2,1,y0,y0),f) is V11() real ext-real Element of REAL

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

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

<*N1,L1*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

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

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

y1 is V16() V19( REAL ) V20( REAL ) Function-like 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

y0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

y0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

partdiff (y0,y0,2) is V11() real ext-real Element of REAL

reproj (2,y0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

y0 * (reproj (2,y0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

(proj (2,2)) . y0 is V11() real ext-real Element of REAL

diff ((y0 * (reproj (2,y0))),((proj (2,2)) . y0)) is V11() real ext-real Element of REAL

(2,2,y0,y0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom (2,2,y0,y0) is V160() V161() V162() Element of K6(REAL)

diff ((2,2,y0,y0),z0) is V11() real ext-real Element of REAL

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

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

<*N1,L1*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

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

R1 is V160() V161() V162() Neighbourhood of L1

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

y1 is V16() V19( REAL ) V20( REAL ) Function-like 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

x0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

y0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

partdiff (y0,x0,1) is V11() real ext-real Element of REAL

reproj (1,x0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

y0 * (reproj (1,x0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

(proj (1,2)) . x0 is V11() real ext-real Element of REAL

diff ((y0 * (reproj (1,x0))),((proj (1,2)) . x0)) is V11() real ext-real Element of REAL

(2,1,y0,x0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

diff ((2,1,y0,x0),f) is V11() real ext-real Element of REAL

dom (2,1,y0,x0) is V160() V161() V162() Element of K6(REAL)

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

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

<*N1,L1*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

(2,1,y0,x0) . N1 is V11() real ext-real Element of REAL

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

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

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

y1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

R1 is V160() V161() V162() Neighbourhood of f

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

y1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

y1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

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

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

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

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

<*L2,R2*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

diff ((2,1,y0,x0),L2) is V11() real ext-real Element of REAL

(2,1,y0,x0) . L2 is V11() real ext-real Element of REAL

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

L12 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

L11 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

L12 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

L11 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

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

R16 is V160() V161() V162() Neighbourhood of f

R18 is V11() real ext-real set

f - R18 is V11() real ext-real Element of REAL

f + R18 is V11() real ext-real Element of REAL

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

{ b

R14 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

R11 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

R11 + 2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

R18 / (R11 + 2) is V11() real ext-real Element of REAL

R14 . R11 is V11() real ext-real Element of REAL

lim R14 is V11() real ext-real Element of REAL

R11 is V1() V16() non-empty V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))

R12 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

R11 . R12 is V11() real ext-real Element of REAL

R12 + 2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

R18 / (R12 + 2) is V11() real ext-real Element of REAL

f + (R18 / (R12 + 2)) is V11() real ext-real Element of REAL

(f + (R18 / (R12 + 2))) - f is V11() real ext-real Element of REAL

R12 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

(R12 + 1) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

0 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

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

- R18 is V11() real ext-real set

f + (- R18) is V11() real ext-real Element of REAL

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

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

(2,1,y0,x0) . R12 is V11() real ext-real Element of REAL

((2,1,y0,x0) . R12) - ((2,1,y0,x0) . f) is V11() real ext-real Element of REAL

R12 - f is V11() real ext-real Element of REAL

x1 . (R12 - f) is V11() real ext-real Element of REAL

y1 . (R12 - f) is V11() real ext-real Element of REAL

(x1 . (R12 - f)) + (y1 . (R12 - f)) is V11() real ext-real Element of REAL

L12 . (R12 - f) is V11() real ext-real Element of REAL

L11 . (R12 - f) is V11() real ext-real Element of REAL

(L12 . (R12 - f)) + (L11 . (R12 - f)) is V11() real ext-real Element of REAL

N2 * (R12 - f) is V11() real ext-real Element of REAL

(N2 * (R12 - f)) + (y1 . (R12 - f)) is V11() real ext-real Element of REAL

(partdiff (y0,x0,1)) * (R12 - f) is V11() real ext-real Element of REAL

((partdiff (y0,x0,1)) * (R12 - f)) + (y1 . (R12 - f)) is V11() real ext-real Element of REAL

(diff ((2,1,y0,x0),L2)) * (R12 - f) is V11() real ext-real Element of REAL

((diff ((2,1,y0,x0),L2)) * (R12 - f)) + (L11 . (R12 - f)) is V11() real ext-real Element of REAL

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

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

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

R12 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

R11 . R12 is V11() real ext-real Element of REAL

(partdiff (y0,x0,1)) * (R11 . R12) is V11() real ext-real Element of REAL

y1 . (R11 . R12) is V11() real ext-real Element of REAL

((partdiff (y0,x0,1)) * (R11 . R12)) + (y1 . (R11 . R12)) is V11() real ext-real Element of REAL

(diff ((2,1,y0,x0),L2)) * (R11 . R12) is V11() real ext-real Element of REAL

L11 . (R11 . R12) is V11() real ext-real Element of REAL

((diff ((2,1,y0,x0),L2)) * (R11 . R12)) + (L11 . (R11 . R12)) is V11() real ext-real Element of REAL

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

R13 - f is V11() real ext-real Element of REAL

((partdiff (y0,x0,1)) * (R11 . R12)) / (R11 . R12) is V11() real ext-real Element of REAL

(y1 . (R11 . R12)) / (R11 . R12) is V11() real ext-real Element of REAL

(((partdiff (y0,x0,1)) * (R11 . R12)) / (R11 . R12)) + ((y1 . (R11 . R12)) / (R11 . R12)) is V11() real ext-real Element of REAL

(((diff ((2,1,y0,x0),L2)) * (R11 . R12)) + (L11 . (R11 . R12))) / (R11 . R12) is V11() real ext-real Element of REAL

(R11 . R12) " is V11() real ext-real Element of REAL

(y1 . (R11 . R12)) * ((R11 . R12) ") is V11() real ext-real Element of REAL

R11 " is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(R11 ") . R12 is V11() real ext-real Element of REAL

(y1 . (R11 . R12)) * ((R11 ") . R12) is V11() real ext-real Element of REAL

y1 /* R11 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(y1 /* R11) . R12 is V11() real ext-real Element of REAL

((y1 /* R11) . R12) * ((R11 ") . R12) is V11() real ext-real Element of REAL

(R11 ") (#) (y1 /* R11) is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

((R11 ") (#) (y1 /* R11)) . R12 is V11() real ext-real Element of REAL

(L11 . (R11 . R12)) / (R11 . R12) is V11() real ext-real Element of REAL

(L11 . (R11 . R12)) * ((R11 . R12) ") is V11() real ext-real Element of REAL

(L11 . (R11 . R12)) * ((R11 ") . R12) is V11() real ext-real Element of REAL

L11 /* R11 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(L11 /* R11) . R12 is V11() real ext-real Element of REAL

((L11 /* R11) . R12) * ((R11 ") . R12) is V11() real ext-real Element of REAL

(R11 ") (#) (L11 /* R11) is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

((R11 ") (#) (L11 /* R11)) . R12 is V11() real ext-real Element of REAL

((diff ((2,1,y0,x0),L2)) * (R11 . R12)) / (R11 . R12) is V11() real ext-real Element of REAL

(R11 . R12) / (R11 . R12) is V11() real ext-real Element of REAL

(diff ((2,1,y0,x0),L2)) * ((R11 . R12) / (R11 . R12)) is V11() real ext-real Element of REAL

(diff ((2,1,y0,x0),L2)) * 1 is V11() real ext-real Element of REAL

(partdiff (y0,x0,1)) * ((R11 . R12) / (R11 . R12)) is V11() real ext-real Element of REAL

(partdiff (y0,x0,1)) * 1 is V11() real ext-real Element of REAL

(partdiff (y0,x0,1)) + ((y1 . (R11 . R12)) / (R11 . R12)) is V11() real ext-real Element of REAL

(diff ((2,1,y0,x0),L2)) + ((L11 . (R11 . R12)) / (R11 . R12)) is V11() real ext-real Element of REAL

(((R11 ") (#) (L11 /* R11)) . R12) - (((R11 ") (#) (y1 /* R11)) . R12) is V11() real ext-real Element of REAL

(diff ((2,1,y0,x0),L2)) + ((((R11 ") (#) (L11 /* R11)) . R12) - (((R11 ") (#) (y1 /* R11)) . R12)) is V11() real ext-real Element of REAL

(partdiff (y0,x0,1)) - (diff ((2,1,y0,x0),L2)) is V11() real ext-real Element of REAL

((R11 ") (#) (L11 /* R11)) - ((R11 ") (#) (y1 /* R11)) is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(((R11 ") (#) (L11 /* R11)) - ((R11 ") (#) (y1 /* R11))) . R12 is V11() real ext-real Element of REAL

(((R11 ") (#) (L11 /* R11)) - ((R11 ") (#) (y1 /* R11))) . 1 is V11() real ext-real Element of REAL

lim (((R11 ") (#) (L11 /* R11)) - ((R11 ") (#) (y1 /* R11))) is V11() real ext-real Element of REAL

lim ((R11 ") (#) (L11 /* R11)) is V11() real ext-real Element of REAL

lim ((R11 ") (#) (y1 /* R11)) is V11() real ext-real Element of REAL

0 - 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional FinSequence-membered 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 V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

x0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

y0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

partdiff (y0,x0,2) is V11() real ext-real Element of REAL

reproj (2,x0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

y0 * (reproj (2,x0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

(proj (2,2)) . x0 is V11() real ext-real Element of REAL

diff ((y0 * (reproj (2,x0))),((proj (2,2)) . x0)) is V11() real ext-real Element of REAL

(2,2,y0,x0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

diff ((2,2,y0,x0),z0) is V11() real ext-real Element of REAL

dom (2,2,y0,x0) is V160() V161() V162() Element of K6(REAL)

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

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

<*N1,L1*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

(2,2,y0,x0) . L1 is V11() real ext-real Element of REAL

(2,2,y0,x0) . z0 is V11() real ext-real Element of REAL

R1 is V160() V161() V162() Neighbourhood of L1

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

y1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

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

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

y1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

y1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

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

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

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

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

<*L2,R2*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

diff ((2,2,y0,x0),R2) is V11() real ext-real Element of REAL

(2,2,y0,x0) . R2 is V11() real ext-real Element of REAL

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

L12 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

L11 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

L12 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

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

L11 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

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

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

R18 is V11() real ext-real set

z0 - R18 is V11() real ext-real Element of REAL

z0 + R18 is V11() real ext-real Element of REAL

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

{ b

R14 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

R11 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

R11 + 2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

R18 / (R11 + 2) is V11() real ext-real Element of REAL

R14 . R11 is V11() real ext-real Element of REAL

lim R14 is V11() real ext-real Element of REAL

R11 is V1() V16() non-empty V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))

R12 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

R11 . R12 is V11() real ext-real Element of REAL

R12 + 2 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

R18 / (R12 + 2) is V11() real ext-real Element of REAL

z0 + (R18 / (R12 + 2)) is V11() real ext-real Element of REAL

(z0 + (R18 / (R12 + 2))) - z0 is V11() real ext-real Element of REAL

R12 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

(R12 + 1) + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

0 + 1 is V1() epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT

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

- R18 is V11() real ext-real set

z0 + (- R18) is V11() real ext-real Element of REAL

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

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

(2,2,y0,x0) . R12 is V11() real ext-real Element of REAL

((2,2,y0,x0) . R12) - ((2,2,y0,x0) . z0) is V11() real ext-real Element of REAL

R12 - z0 is V11() real ext-real Element of REAL

x1 . (R12 - z0) is V11() real ext-real Element of REAL

y1 . (R12 - z0) is V11() real ext-real Element of REAL

(x1 . (R12 - z0)) + (y1 . (R12 - z0)) is V11() real ext-real Element of REAL

L12 . (R12 - z0) is V11() real ext-real Element of REAL

L11 . (R12 - z0) is V11() real ext-real Element of REAL

(L12 . (R12 - z0)) + (L11 . (R12 - z0)) is V11() real ext-real Element of REAL

N2 * (R12 - z0) is V11() real ext-real Element of REAL

(N2 * (R12 - z0)) + (y1 . (R12 - z0)) is V11() real ext-real Element of REAL

(partdiff (y0,x0,2)) * (R12 - z0) is V11() real ext-real Element of REAL

((partdiff (y0,x0,2)) * (R12 - z0)) + (y1 . (R12 - z0)) is V11() real ext-real Element of REAL

(diff ((2,2,y0,x0),R2)) * (R12 - z0) is V11() real ext-real Element of REAL

((diff ((2,2,y0,x0),R2)) * (R12 - z0)) + (L11 . (R12 - z0)) is V11() real ext-real Element of REAL

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

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

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

R12 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

R11 . R12 is V11() real ext-real Element of REAL

(partdiff (y0,x0,2)) * (R11 . R12) is V11() real ext-real Element of REAL

y1 . (R11 . R12) is V11() real ext-real Element of REAL

((partdiff (y0,x0,2)) * (R11 . R12)) + (y1 . (R11 . R12)) is V11() real ext-real Element of REAL

(diff ((2,2,y0,x0),R2)) * (R11 . R12) is V11() real ext-real Element of REAL

L11 . (R11 . R12) is V11() real ext-real Element of REAL

((diff ((2,2,y0,x0),R2)) * (R11 . R12)) + (L11 . (R11 . R12)) is V11() real ext-real Element of REAL

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

R13 - z0 is V11() real ext-real Element of REAL

((partdiff (y0,x0,2)) * (R11 . R12)) / (R11 . R12) is V11() real ext-real Element of REAL

(y1 . (R11 . R12)) / (R11 . R12) is V11() real ext-real Element of REAL

(((partdiff (y0,x0,2)) * (R11 . R12)) / (R11 . R12)) + ((y1 . (R11 . R12)) / (R11 . R12)) is V11() real ext-real Element of REAL

(((diff ((2,2,y0,x0),R2)) * (R11 . R12)) + (L11 . (R11 . R12))) / (R11 . R12) is V11() real ext-real Element of REAL

(R11 . R12) " is V11() real ext-real Element of REAL

(y1 . (R11 . R12)) * ((R11 . R12) ") is V11() real ext-real Element of REAL

R11 " is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(R11 ") . R12 is V11() real ext-real Element of REAL

(y1 . (R11 . R12)) * ((R11 ") . R12) is V11() real ext-real Element of REAL

y1 /* R11 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(y1 /* R11) . R12 is V11() real ext-real Element of REAL

((y1 /* R11) . R12) * ((R11 ") . R12) is V11() real ext-real Element of REAL

(R11 ") (#) (y1 /* R11) is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

((R11 ") (#) (y1 /* R11)) . R12 is V11() real ext-real Element of REAL

(L11 . (R11 . R12)) / (R11 . R12) is V11() real ext-real Element of REAL

(L11 . (R11 . R12)) * ((R11 . R12) ") is V11() real ext-real Element of REAL

(L11 . (R11 . R12)) * ((R11 ") . R12) is V11() real ext-real Element of REAL

L11 /* R11 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(L11 /* R11) . R12 is V11() real ext-real Element of REAL

((L11 /* R11) . R12) * ((R11 ") . R12) is V11() real ext-real Element of REAL

(R11 ") (#) (L11 /* R11) is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

((R11 ") (#) (L11 /* R11)) . R12 is V11() real ext-real Element of REAL

((diff ((2,2,y0,x0),R2)) * (R11 . R12)) / (R11 . R12) is V11() real ext-real Element of REAL

(R11 . R12) / (R11 . R12) is V11() real ext-real Element of REAL

(diff ((2,2,y0,x0),R2)) * ((R11 . R12) / (R11 . R12)) is V11() real ext-real Element of REAL

(diff ((2,2,y0,x0),R2)) * 1 is V11() real ext-real Element of REAL

(partdiff (y0,x0,2)) * ((R11 . R12) / (R11 . R12)) is V11() real ext-real Element of REAL

(partdiff (y0,x0,2)) * 1 is V11() real ext-real Element of REAL

(partdiff (y0,x0,2)) + ((y1 . (R11 . R12)) / (R11 . R12)) is V11() real ext-real Element of REAL

(diff ((2,2,y0,x0),R2)) + ((L11 . (R11 . R12)) / (R11 . R12)) is V11() real ext-real Element of REAL

(((R11 ") (#) (L11 /* R11)) . R12) - (((R11 ") (#) (y1 /* R11)) . R12) is V11() real ext-real Element of REAL

(diff ((2,2,y0,x0),R2)) + ((((R11 ") (#) (L11 /* R11)) . R12) - (((R11 ") (#) (y1 /* R11)) . R12)) is V11() real ext-real Element of REAL

(partdiff (y0,x0,2)) - (diff ((2,2,y0,x0),R2)) is V11() real ext-real Element of REAL

((R11 ") (#) (L11 /* R11)) - ((R11 ") (#) (y1 /* R11)) is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

(((R11 ") (#) (L11 /* R11)) - ((R11 ") (#) (y1 /* R11))) . R12 is V11() real ext-real Element of REAL

(((R11 ") (#) (L11 /* R11)) - ((R11 ") (#) (y1 /* R11))) . 1 is V11() real ext-real Element of REAL

lim (((R11 ") (#) (L11 /* R11)) - ((R11 ") (#) (y1 /* R11))) is V11() real ext-real Element of REAL

lim ((R11 ") (#) (L11 /* R11)) is V11() real ext-real Element of REAL

lim ((R11 ") (#) (y1 /* R11)) is V11() real ext-real Element of REAL

0 - 0 is V1() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional FinSequence-membered V160() V161() V162() V163() V164() V165() V166() Element of REAL

f is functional FinSequence-membered Element of K6((REAL 2))

z0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

dom z0 is functional FinSequence-membered Element of K6((REAL 2))

z0 | f is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

y0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

(2,1,(z0 | f),y0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

reproj (1,y0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

(z0 | f) * (reproj (1,y0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom (2,1,(z0 | f),y0) is V160() V161() V162() Element of K6(REAL)

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

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

<*y0,N1*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

(2,1,(z0 | f),y0) . y0 is V11() real ext-real Element of REAL

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

R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

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

R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

(2,1,z0,y0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

z0 * (reproj (1,y0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

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

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

(2,1,z0,y0) . y1 is V11() real ext-real Element of REAL

((2,1,z0,y0) . y1) - ((2,1,z0,y0) . y0) is V11() real ext-real Element of REAL

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

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

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

(R1 . (y1 - y0)) + (x1 . (y1 - y0)) is V11() real ext-real Element of REAL

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

(2,1,(z0 | f),y0) . N2 is V11() real ext-real Element of REAL

(2,1,z0,y0) . N2 is V11() real ext-real Element of REAL

dom (reproj (1,y0)) is V160() V161() V162() Element of K6(REAL)

(reproj (1,y0)) . N2 is V61(2) FinSequence-like Element of REAL 2

dom (z0 | f) is functional FinSequence-membered Element of K6((REAL 2))

(z0 | f) . ((reproj (1,y0)) . N2) is V11() real ext-real Element of REAL

z0 . ((reproj (1,y0)) . N2) is V11() real ext-real Element of REAL

(2,1,(z0 | f),y0) . y1 is V11() real ext-real Element of REAL

((2,1,(z0 | f),y0) . y1) - ((2,1,(z0 | f),y0) . y0) is V11() real ext-real Element of REAL

((2,1,z0,y0) . y1) - ((2,1,(z0 | f),y0) . y0) is V11() real ext-real Element of REAL

dom (2,1,z0,y0) is V160() V161() V162() Element of K6(REAL)

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

dom (z0 | f) is functional FinSequence-membered Element of K6((REAL 2))

(dom z0) /\ f is functional FinSequence-membered Element of K6((REAL 2))

dom (reproj (1,y0)) is V160() V161() V162() Element of K6(REAL)

(reproj (1,y0)) . y1 is V61(2) FinSequence-like Element of REAL 2

y1 is set

f is functional FinSequence-membered Element of K6((REAL 2))

z0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

dom z0 is functional FinSequence-membered Element of K6((REAL 2))

z0 | f is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

y0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

(2,2,(z0 | f),y0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

reproj (2,y0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

(z0 | f) * (reproj (2,y0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom (2,2,(z0 | f),y0) is V160() V161() V162() Element of K6(REAL)

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

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

<*y0,N1*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set

(2,2,(z0 | f),y0) . N1 is V11() real ext-real Element of REAL

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

R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

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

R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))

x1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))

(2,2,z0,y0) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

z0 * (reproj (2,y0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

(2,2,z0,y0) . N1 is V11() real ext-real Element of REAL

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

(2,2,z0,y0) . y1 is V11() real ext-real Element of REAL

((2,2,z0,y0) . y1) - ((2,2,z0,y0) . N1) is V11() real ext-real Element of REAL

y1 - N1 is V11() real ext-real Element of REAL

R1 . (y1 - N1) is V11() real ext-real Element of REAL

x1 . (y1 - N1) is V11() real ext-real Element of REAL

(R1 . (y1 - N1)) + (x1 . (y1 - N1)) is V11() real ext-real Element of REAL

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

(2,2,(z0 | f),y0) . N2 is V11() real ext-real Element of REAL

(2,2,z0,y0) . N2 is V11() real ext-real Element of REAL

dom (reproj (2,y0)) is V160() V161() V162() Element of K6(REAL)

(reproj (2,y0)) . N2 is V61(2) FinSequence-like Element of REAL 2

dom (z0 | f) is functional FinSequence-membered Element of K6((REAL 2))

(z0 | f) . ((reproj (2,y0)) . N2) is V11() real ext-real Element of REAL

z0 . ((reproj (2,y0)) . N2) is V11() real ext-real Element of REAL

(2,2,(z0 | f),y0) . y1 is V11() real ext-real Element of REAL

((2,2,(z0 | f),y0) . y1) - ((2,2,(z0 | f),y0) . N1) is V11() real ext-real Element of REAL

((2,2,z0,y0) . y1) - ((2,2,(z0 | f),y0) . N1) is V11() real ext-real Element of REAL

dom (2,2,z0,y0) is V160() V161() V162() Element of K6(REAL)

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

dom (z0 | f) is functional FinSequence-membered Element of K6((REAL 2))

(dom z0) /\ f is functional FinSequence-membered Element of K6((REAL 2))

dom (reproj (2,y0)) is V160() V161() V162() Element of K6(REAL)

(reproj (2,y0)) . y1 is V61(2) FinSequence-like Element of REAL 2

y1 is set

f is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

z0 is set

x0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

dom x0 is functional FinSequence-membered Element of K6((REAL 2))

dom f is functional FinSequence-membered Element of K6((REAL 2))

y0 is set

y0 is set

y0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

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

partdiff (f,y0,1) is V11() real ext-real Element of REAL

reproj (1,y0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

f * (reproj (1,y0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

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

diff ((f * (reproj (1,y0))),((proj (1,2)) . y0)) is V11() real ext-real Element of REAL

x0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

dom x0 is functional FinSequence-membered Element of K6((REAL 2))

y0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

dom y0 is functional FinSequence-membered Element of K6((REAL 2))

y0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

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

partdiff (f,y0,1) is V11() real ext-real Element of REAL

reproj (1,y0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

f * (reproj (1,y0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

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

diff ((f * (reproj (1,y0))),((proj (1,2)) . y0)) is V11() real ext-real Element of REAL

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

f is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

z0 is set

x0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

dom x0 is functional FinSequence-membered Element of K6((REAL 2))

dom f is functional FinSequence-membered Element of K6((REAL 2))

y0 is set

y0 is set

y0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

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

partdiff (f,y0,2) is V11() real ext-real Element of REAL

reproj (2,y0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

f * (reproj (2,y0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

(proj (2,2)) . y0 is V11() real ext-real Element of REAL

diff ((f * (reproj (2,y0))),((proj (2,2)) . y0)) is V11() real ext-real Element of REAL

x0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

dom x0 is functional FinSequence-membered Element of K6((REAL 2))

y0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

dom y0 is functional FinSequence-membered Element of K6((REAL 2))

y0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

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

partdiff (f,y0,2) is V11() real ext-real Element of REAL

reproj (2,y0) is V1() V16() V19( REAL ) V20( REAL 2) Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))

K7(REAL,(REAL 2)) is set

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

f * (reproj (2,y0)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

(proj (2,2)) . y0 is V11() real ext-real Element of REAL

diff ((f * (reproj (2,y0))),((proj (2,2)) . y0)) is V11() real ext-real Element of REAL

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

f is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),REAL))

z0 is V16() V19( NAT ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued V54() V61(2) FinSequence-like FinSubsequence-like Element of REAL 2

(proj (1,2)) . z0 is V11() real ext-real