:: 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₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= f - R18 & not f + R18 <= b₁ ) } is set
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₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= z0 - R18 & not z0 + R18 <= b₁ ) } is set
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 Element of REAL
(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)
{((proj (1,2)) . z0)} is V1() V160() V161() V162() set
partdiff (f,z0,1) is V11() real ext-real Element of REAL
diff ((f * (reproj (1,z0))),((proj (1,2)) . z0)) is V11() real ext-real Element of REAL
x0 is V160() V161() V162() Neighbourhood of (proj (1,2)) . z0
y0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*y0,y0*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set
(2,1,f,z0) . y0 is V11() real ext-real Element of REAL
N1 is V160() V161() V162() Neighbourhood of y0
L1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N1 is V160() V161() V162() Neighbourhood of y0
L1 is V160() V161() V162() Neighbourhood of y0
R1 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))
R1 " 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))
x1 is V1() V16() V19( NAT ) V20( REAL ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent Element of K6(K7(NAT,REAL))
rng x1 is V160() V161() V162() Element of K6(REAL)
R1 + x1 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))
rng (R1 + x1) is V160() V161() V162() Element of K6(REAL)
(2,1,f,z0) /* (R1 + x1) 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))
(2,1,f,z0) /* x1 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))
((2,1,f,z0) /* (R1 + x1)) - ((2,1,f,z0) /* x1) 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))
(R1 ") (#) (((2,1,f,z0) /* (R1 + x1)) - ((2,1,f,z0) /* x1)) 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))
lim ((R1 ") (#) (((2,1,f,z0) /* (R1 + x1)) - ((2,1,f,z0) /* x1))) is V11() real ext-real Element of REAL
y1 is V11() real ext-real set
y0 - y1 is V11() real ext-real Element of REAL
y0 + y1 is V11() real ext-real Element of REAL
].(y0 - y1),(y0 + y1).[ is V160() V161() V162() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= y0 - y1 & not y0 + y1 <= b₁ ) } is set
y0 + 0 is V11() real ext-real Element of REAL
y0 - 0 is V11() real ext-real Element of REAL
N2 is set
lim x1 is V11() real ext-real Element of REAL
lim R1 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
lim (R1 + x1) is V11() real ext-real Element of REAL
0 + y0 is V11() real ext-real Element of REAL
N2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
x1 ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent subsequence of x1
rng (x1 ^\ N2) is V160() V161() V162() Element of K6(REAL)
(R1 + x1) ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of R1 + x1
rng ((R1 + x1) ^\ N2) is V160() V161() V162() Element of K6(REAL)
{y0} is V1() V160() V161() V162() set
L2 is set
L2 is set
R2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
((R1 + x1) ^\ N2) . R2 is V11() real ext-real Element of REAL
N2 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
N2 + R2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
(R1 + x1) . (N2 + R2) is V11() real ext-real Element of REAL
((R1 + x1) . (N2 + R2)) - y0 is V11() real ext-real Element of REAL
abs (((R1 + x1) . (N2 + R2)) - y0) is V11() real ext-real Element of REAL
R2 + N2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
(R1 + x1) . (R2 + N2) is V11() real ext-real Element of REAL
((R1 + x1) . (R2 + N2)) - y0 is V11() real ext-real Element of REAL
(((R1 + x1) ^\ N2) . R2) - y0 is V11() real ext-real Element of REAL
- y1 is V11() real ext-real set
y0 + (- y1) is V11() real ext-real Element of REAL
N2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
x1 ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent subsequence of x1
rng (x1 ^\ N2) is V160() V161() V162() Element of K6(REAL)
(R1 + x1) ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of R1 + x1
rng ((R1 + x1) ^\ N2) is V160() V161() V162() Element of K6(REAL)
N2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
x1 ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent subsequence of x1
rng (x1 ^\ N2) is V160() V161() V162() Element of K6(REAL)
(R1 + x1) ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of R1 + x1
rng ((R1 + x1) ^\ N2) is V160() V161() V162() Element of K6(REAL)
L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is set
R1 ^\ N2 is V1() V16() non-empty V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent subsequence of R1
L2 /* (R1 ^\ N2) 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))
R2 /* (R1 ^\ N2) 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))
(L2 /* (R1 ^\ N2)) + (R2 /* (R1 ^\ N2)) 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))
(R1 ^\ N2) " 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))
((L2 /* (R1 ^\ N2)) + (R2 /* (R1 ^\ N2))) (#) ((R1 ^\ N2) ") 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))
lim (((L2 /* (R1 ^\ N2)) + (R2 /* (R1 ^\ N2))) (#) ((R1 ^\ N2) ")) is V11() real ext-real Element of REAL
L2 . 1 is V11() real ext-real Element of REAL
(R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ") 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))
N 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))
((R1 ^\ N2) ") (#) (R2 /* (R1 ^\ N2)) 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))
lim (((R1 ^\ N2) ") (#) (R2 /* (R1 ^\ N2))) is V11() real ext-real Element of REAL
L12 is V11() real ext-real set
L11 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
R16 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
N . R16 is V11() real ext-real Element of REAL
(N . R16) - (L2 . 1) is V11() real ext-real Element of REAL
abs ((N . R16) - (L2 . 1)) is V11() real ext-real Element of REAL
((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . R16 is V11() real ext-real Element of REAL
(L2 . 1) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . R16) is V11() real ext-real Element of REAL
((L2 . 1) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . R16)) - (L2 . 1) is V11() real ext-real Element of REAL
abs (((L2 . 1) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . R16)) - (L2 . 1)) is V11() real ext-real Element of REAL
(((R1 ^\ N2) ") (#) (R2 /* (R1 ^\ N2))) . R16 is V11() real ext-real Element of REAL
((((R1 ^\ N2) ") (#) (R2 /* (R1 ^\ N2))) . R16) - 0 is V11() real ext-real Element of REAL
abs (((((R1 ^\ N2) ") (#) (R2 /* (R1 ^\ N2))) . R16) - 0) is V11() real ext-real Element of REAL
L12 is V11() real ext-real Element of REAL
L12 * 1 is V11() real ext-real Element of REAL
L11 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
(R1 ^\ N2) . L11 is V11() real ext-real Element of REAL
(((L2 /* (R1 ^\ N2)) + (R2 /* (R1 ^\ N2))) (#) ((R1 ^\ N2) ")) . L11 is V11() real ext-real Element of REAL
((L2 /* (R1 ^\ N2)) + (R2 /* (R1 ^\ N2))) . L11 is V11() real ext-real Element of REAL
((R1 ^\ N2) ") . L11 is V11() real ext-real Element of REAL
(((L2 /* (R1 ^\ N2)) + (R2 /* (R1 ^\ N2))) . L11) * (((R1 ^\ N2) ") . L11) is V11() real ext-real Element of REAL
(L2 /* (R1 ^\ N2)) . L11 is V11() real ext-real Element of REAL
(R2 /* (R1 ^\ N2)) . L11 is V11() real ext-real Element of REAL
((L2 /* (R1 ^\ N2)) . L11) + ((R2 /* (R1 ^\ N2)) . L11) is V11() real ext-real Element of REAL
(((L2 /* (R1 ^\ N2)) . L11) + ((R2 /* (R1 ^\ N2)) . L11)) * (((R1 ^\ N2) ") . L11) is V11() real ext-real Element of REAL
((L2 /* (R1 ^\ N2)) . L11) * (((R1 ^\ N2) ") . L11) is V11() real ext-real Element of REAL
((R2 /* (R1 ^\ N2)) . L11) * (((R1 ^\ N2) ") . L11) is V11() real ext-real Element of REAL
(((L2 /* (R1 ^\ N2)) . L11) * (((R1 ^\ N2) ") . L11)) + (((R2 /* (R1 ^\ N2)) . L11) * (((R1 ^\ N2) ") . L11)) is V11() real ext-real Element of REAL
((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . L11 is V11() real ext-real Element of REAL
(((L2 /* (R1 ^\ N2)) . L11) * (((R1 ^\ N2) ") . L11)) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . L11) is V11() real ext-real Element of REAL
((R1 ^\ N2) . L11) " is V11() real ext-real Element of REAL
((L2 /* (R1 ^\ N2)) . L11) * (((R1 ^\ N2) . L11) ") is V11() real ext-real Element of REAL
(((L2 /* (R1 ^\ N2)) . L11) * (((R1 ^\ N2) . L11) ")) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . L11) is V11() real ext-real Element of REAL
L2 . ((R1 ^\ N2) . L11) is V11() real ext-real Element of REAL
(L2 . ((R1 ^\ N2) . L11)) * (((R1 ^\ N2) . L11) ") is V11() real ext-real Element of REAL
((L2 . ((R1 ^\ N2) . L11)) * (((R1 ^\ N2) . L11) ")) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . L11) is V11() real ext-real Element of REAL
L12 * ((R1 ^\ N2) . L11) is V11() real ext-real Element of REAL
(L12 * ((R1 ^\ N2) . L11)) * (((R1 ^\ N2) . L11) ") is V11() real ext-real Element of REAL
((L12 * ((R1 ^\ N2) . L11)) * (((R1 ^\ N2) . L11) ")) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . L11) is V11() real ext-real Element of REAL
((R1 ^\ N2) . L11) * (((R1 ^\ N2) . L11) ") is V11() real ext-real Element of REAL
L12 * (((R1 ^\ N2) . L11) * (((R1 ^\ N2) . L11) ")) is V11() real ext-real Element of REAL
(L12 * (((R1 ^\ N2) . L11) * (((R1 ^\ N2) . L11) "))) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . L11) is V11() real ext-real Element of REAL
(L12 * 1) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . L11) is V11() real ext-real Element of REAL
N . L11 is V11() real ext-real Element of REAL
N is set
N is set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
((R1 + x1) ^\ N2) . N is V11() real ext-real Element of REAL
(2,1,f,z0) . (((R1 + x1) ^\ N2) . N) is V11() real ext-real Element of REAL
(x1 ^\ N2) . N is V11() real ext-real Element of REAL
(2,1,f,z0) . ((x1 ^\ N2) . N) is V11() real ext-real Element of REAL
((2,1,f,z0) . (((R1 + x1) ^\ N2) . N)) - ((2,1,f,z0) . ((x1 ^\ N2) . N)) is V11() real ext-real Element of REAL
(R1 ^\ N2) . N is V11() real ext-real Element of REAL
L2 . ((R1 ^\ N2) . N) is V11() real ext-real Element of REAL
R2 . ((R1 ^\ N2) . N) is V11() real ext-real Element of REAL
(L2 . ((R1 ^\ N2) . N)) + (R2 . ((R1 ^\ N2) . N)) is V11() real ext-real Element of REAL
(((R1 + x1) ^\ N2) . N) - ((x1 ^\ N2) . N) is V11() real ext-real Element of REAL
(R1 ^\ N2) + (x1 ^\ N2) 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))
((R1 ^\ N2) + (x1 ^\ N2)) . N is V11() real ext-real Element of REAL
(((R1 ^\ N2) + (x1 ^\ N2)) . N) - ((x1 ^\ N2) . N) is V11() real ext-real Element of REAL
((R1 ^\ N2) . N) + ((x1 ^\ N2) . N) is V11() real ext-real Element of REAL
(((R1 ^\ N2) . N) + ((x1 ^\ N2) . N)) - ((x1 ^\ N2) . N) is V11() real ext-real Element of REAL
(2,1,f,z0) /* ((R1 + x1) ^\ N2) 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))
(2,1,f,z0) /* (x1 ^\ N2) 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))
((2,1,f,z0) /* ((R1 + x1) ^\ N2)) - ((2,1,f,z0) /* (x1 ^\ N2)) 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))
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
(((2,1,f,z0) /* ((R1 + x1) ^\ N2)) - ((2,1,f,z0) /* (x1 ^\ N2))) . N is V11() real ext-real Element of REAL
((2,1,f,z0) /* ((R1 + x1) ^\ N2)) . N is V11() real ext-real Element of REAL
((2,1,f,z0) /* (x1 ^\ N2)) . N is V11() real ext-real Element of REAL
(((2,1,f,z0) /* ((R1 + x1) ^\ N2)) . N) - (((2,1,f,z0) /* (x1 ^\ N2)) . N) is V11() real ext-real Element of REAL
((R1 + x1) ^\ N2) . N is V11() real ext-real Element of REAL
(2,1,f,z0) . (((R1 + x1) ^\ N2) . N) is V11() real ext-real Element of REAL
((2,1,f,z0) . (((R1 + x1) ^\ N2) . N)) - (((2,1,f,z0) /* (x1 ^\ N2)) . N) is V11() real ext-real Element of REAL
(x1 ^\ N2) . N is V11() real ext-real Element of REAL
(2,1,f,z0) . ((x1 ^\ N2) . N) is V11() real ext-real Element of REAL
((2,1,f,z0) . (((R1 + x1) ^\ N2) . N)) - ((2,1,f,z0) . ((x1 ^\ N2) . N)) is V11() real ext-real Element of REAL
(R1 ^\ N2) . N is V11() real ext-real Element of REAL
L2 . ((R1 ^\ N2) . N) is V11() real ext-real Element of REAL
R2 . ((R1 ^\ N2) . N) is V11() real ext-real Element of REAL
(L2 . ((R1 ^\ N2) . N)) + (R2 . ((R1 ^\ N2) . N)) is V11() real ext-real Element of REAL
(L2 /* (R1 ^\ N2)) . N is V11() real ext-real Element of REAL
((L2 /* (R1 ^\ N2)) . N) + (R2 . ((R1 ^\ N2) . N)) is V11() real ext-real Element of REAL
(R2 /* (R1 ^\ N2)) . N is V11() real ext-real Element of REAL
((L2 /* (R1 ^\ N2)) . N) + ((R2 /* (R1 ^\ N2)) . N) is V11() real ext-real Element of REAL
((L2 /* (R1 ^\ N2)) + (R2 /* (R1 ^\ N2))) . N is V11() real ext-real Element of REAL
((2,1,f,z0) /* (R1 + x1)) ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of (2,1,f,z0) /* (R1 + x1)
(((2,1,f,z0) /* (R1 + x1)) ^\ N2) - ((2,1,f,z0) /* (x1 ^\ N2)) 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))
((((2,1,f,z0) /* (R1 + x1)) ^\ N2) - ((2,1,f,z0) /* (x1 ^\ N2))) (#) ((R1 ^\ N2) ") 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))
((2,1,f,z0) /* x1) ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of (2,1,f,z0) /* x1
(((2,1,f,z0) /* (R1 + x1)) ^\ N2) - (((2,1,f,z0) /* x1) ^\ N2) 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))
((((2,1,f,z0) /* (R1 + x1)) ^\ N2) - (((2,1,f,z0) /* x1) ^\ N2)) (#) ((R1 ^\ N2) ") 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))
(((2,1,f,z0) /* (R1 + x1)) - ((2,1,f,z0) /* x1)) ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of ((2,1,f,z0) /* (R1 + x1)) - ((2,1,f,z0) /* x1)
((((2,1,f,z0) /* (R1 + x1)) - ((2,1,f,z0) /* x1)) ^\ N2) (#) ((R1 ^\ N2) ") 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))
(R1 ") ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of R1 "
((((2,1,f,z0) /* (R1 + x1)) - ((2,1,f,z0) /* x1)) ^\ N2) (#) ((R1 ") ^\ N2) 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))
(((2,1,f,z0) /* (R1 + x1)) - ((2,1,f,z0) /* x1)) (#) (R1 ") 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))
((((2,1,f,z0) /* (R1 + x1)) - ((2,1,f,z0) /* x1)) (#) (R1 ")) ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of (((2,1,f,z0) /* (R1 + x1)) - ((2,1,f,z0) /* x1)) (#) (R1 ")
N is V11() real ext-real Element of REAL
(2,1,f,z0) . N is V11() real ext-real Element of REAL
((2,1,f,z0) . N) - ((2,1,f,z0) . y0) is V11() real ext-real Element of REAL
N - y0 is V11() real ext-real Element of REAL
L2 . (N - y0) is V11() real ext-real Element of REAL
R2 . (N - y0) is V11() real ext-real Element of REAL
(L2 . (N - y0)) + (R2 . (N - 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 (2,2)) . z0 is V11() real ext-real Element of REAL
(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)
{((proj (2,2)) . z0)} is V1() V160() V161() V162() set
partdiff (f,z0,2) is V11() real ext-real Element of REAL
diff ((f * (reproj (2,z0))),((proj (2,2)) . z0)) is V11() real ext-real Element of REAL
x0 is V160() V161() V162() Neighbourhood of (proj (2,2)) . z0
y0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*y0,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
N1 is V160() V161() V162() Neighbourhood of y0
L1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N1 is V160() V161() V162() Neighbourhood of y0
L1 is V160() V161() V162() Neighbourhood of y0
R1 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))
R1 " 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))
x1 is V1() V16() V19( NAT ) V20( REAL ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent Element of K6(K7(NAT,REAL))
rng x1 is V160() V161() V162() Element of K6(REAL)
R1 + x1 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))
rng (R1 + x1) is V160() V161() V162() Element of K6(REAL)
(2,2,f,z0) /* (R1 + x1) 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))
(2,2,f,z0) /* x1 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))
((2,2,f,z0) /* (R1 + x1)) - ((2,2,f,z0) /* x1) 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))
(R1 ") (#) (((2,2,f,z0) /* (R1 + x1)) - ((2,2,f,z0) /* x1)) 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))
lim ((R1 ") (#) (((2,2,f,z0) /* (R1 + x1)) - ((2,2,f,z0) /* x1))) is V11() real ext-real Element of REAL
y1 is V11() real ext-real set
y0 - y1 is V11() real ext-real Element of REAL
y0 + y1 is V11() real ext-real Element of REAL
].(y0 - y1),(y0 + y1).[ is V160() V161() V162() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= y0 - y1 & not y0 + y1 <= b₁ ) } is set
y0 + 0 is V11() real ext-real Element of REAL
y0 - 0 is V11() real ext-real Element of REAL
N2 is set
lim x1 is V11() real ext-real Element of REAL
lim R1 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
lim (R1 + x1) is V11() real ext-real Element of REAL
0 + y0 is V11() real ext-real Element of REAL
N2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
x1 ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent subsequence of x1
rng (x1 ^\ N2) is V160() V161() V162() Element of K6(REAL)
(R1 + x1) ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of R1 + x1
rng ((R1 + x1) ^\ N2) is V160() V161() V162() Element of K6(REAL)
{y0} is V1() V160() V161() V162() set
L2 is set
L2 is set
R2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
((R1 + x1) ^\ N2) . R2 is V11() real ext-real Element of REAL
N2 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
N2 + R2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
(R1 + x1) . (N2 + R2) is V11() real ext-real Element of REAL
((R1 + x1) . (N2 + R2)) - y0 is V11() real ext-real Element of REAL
abs (((R1 + x1) . (N2 + R2)) - y0) is V11() real ext-real Element of REAL
R2 + N2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
(R1 + x1) . (R2 + N2) is V11() real ext-real Element of REAL
((R1 + x1) . (R2 + N2)) - y0 is V11() real ext-real Element of REAL
(((R1 + x1) ^\ N2) . R2) - y0 is V11() real ext-real Element of REAL
- y1 is V11() real ext-real set
y0 + (- y1) is V11() real ext-real Element of REAL
N2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
x1 ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent subsequence of x1
rng (x1 ^\ N2) is V160() V161() V162() Element of K6(REAL)
(R1 + x1) ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of R1 + x1
rng ((R1 + x1) ^\ N2) is V160() V161() V162() Element of K6(REAL)
N2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
x1 ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like constant total quasi_total complex-valued ext-real-valued real-valued convergent subsequence of x1
rng (x1 ^\ N2) is V160() V161() V162() Element of K6(REAL)
(R1 + x1) ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of R1 + x1
rng ((R1 + x1) ^\ N2) is V160() V161() V162() Element of K6(REAL)
L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is set
R1 ^\ N2 is V1() V16() non-empty V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent subsequence of R1
L2 /* (R1 ^\ N2) 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))
R2 /* (R1 ^\ N2) 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))
(L2 /* (R1 ^\ N2)) + (R2 /* (R1 ^\ N2)) 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))
(R1 ^\ N2) " 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))
((L2 /* (R1 ^\ N2)) + (R2 /* (R1 ^\ N2))) (#) ((R1 ^\ N2) ") 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))
lim (((L2 /* (R1 ^\ N2)) + (R2 /* (R1 ^\ N2))) (#) ((R1 ^\ N2) ")) is V11() real ext-real Element of REAL
L2 . 1 is V11() real ext-real Element of REAL
(R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ") 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))
N 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))
((R1 ^\ N2) ") (#) (R2 /* (R1 ^\ N2)) 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))
lim (((R1 ^\ N2) ") (#) (R2 /* (R1 ^\ N2))) is V11() real ext-real Element of REAL
L12 is V11() real ext-real set
L11 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
R16 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
N . R16 is V11() real ext-real Element of REAL
(N . R16) - (L2 . 1) is V11() real ext-real Element of REAL
abs ((N . R16) - (L2 . 1)) is V11() real ext-real Element of REAL
((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . R16 is V11() real ext-real Element of REAL
(L2 . 1) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . R16) is V11() real ext-real Element of REAL
((L2 . 1) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . R16)) - (L2 . 1) is V11() real ext-real Element of REAL
abs (((L2 . 1) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . R16)) - (L2 . 1)) is V11() real ext-real Element of REAL
(((R1 ^\ N2) ") (#) (R2 /* (R1 ^\ N2))) . R16 is V11() real ext-real Element of REAL
((((R1 ^\ N2) ") (#) (R2 /* (R1 ^\ N2))) . R16) - 0 is V11() real ext-real Element of REAL
abs (((((R1 ^\ N2) ") (#) (R2 /* (R1 ^\ N2))) . R16) - 0) is V11() real ext-real Element of REAL
L12 is V11() real ext-real Element of REAL
L12 * 1 is V11() real ext-real Element of REAL
L11 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
(R1 ^\ N2) . L11 is V11() real ext-real Element of REAL
(((L2 /* (R1 ^\ N2)) + (R2 /* (R1 ^\ N2))) (#) ((R1 ^\ N2) ")) . L11 is V11() real ext-real Element of REAL
((L2 /* (R1 ^\ N2)) + (R2 /* (R1 ^\ N2))) . L11 is V11() real ext-real Element of REAL
((R1 ^\ N2) ") . L11 is V11() real ext-real Element of REAL
(((L2 /* (R1 ^\ N2)) + (R2 /* (R1 ^\ N2))) . L11) * (((R1 ^\ N2) ") . L11) is V11() real ext-real Element of REAL
(L2 /* (R1 ^\ N2)) . L11 is V11() real ext-real Element of REAL
(R2 /* (R1 ^\ N2)) . L11 is V11() real ext-real Element of REAL
((L2 /* (R1 ^\ N2)) . L11) + ((R2 /* (R1 ^\ N2)) . L11) is V11() real ext-real Element of REAL
(((L2 /* (R1 ^\ N2)) . L11) + ((R2 /* (R1 ^\ N2)) . L11)) * (((R1 ^\ N2) ") . L11) is V11() real ext-real Element of REAL
((L2 /* (R1 ^\ N2)) . L11) * (((R1 ^\ N2) ") . L11) is V11() real ext-real Element of REAL
((R2 /* (R1 ^\ N2)) . L11) * (((R1 ^\ N2) ") . L11) is V11() real ext-real Element of REAL
(((L2 /* (R1 ^\ N2)) . L11) * (((R1 ^\ N2) ") . L11)) + (((R2 /* (R1 ^\ N2)) . L11) * (((R1 ^\ N2) ") . L11)) is V11() real ext-real Element of REAL
((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . L11 is V11() real ext-real Element of REAL
(((L2 /* (R1 ^\ N2)) . L11) * (((R1 ^\ N2) ") . L11)) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . L11) is V11() real ext-real Element of REAL
((R1 ^\ N2) . L11) " is V11() real ext-real Element of REAL
((L2 /* (R1 ^\ N2)) . L11) * (((R1 ^\ N2) . L11) ") is V11() real ext-real Element of REAL
(((L2 /* (R1 ^\ N2)) . L11) * (((R1 ^\ N2) . L11) ")) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . L11) is V11() real ext-real Element of REAL
L2 . ((R1 ^\ N2) . L11) is V11() real ext-real Element of REAL
(L2 . ((R1 ^\ N2) . L11)) * (((R1 ^\ N2) . L11) ") is V11() real ext-real Element of REAL
((L2 . ((R1 ^\ N2) . L11)) * (((R1 ^\ N2) . L11) ")) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . L11) is V11() real ext-real Element of REAL
L12 * ((R1 ^\ N2) . L11) is V11() real ext-real Element of REAL
(L12 * ((R1 ^\ N2) . L11)) * (((R1 ^\ N2) . L11) ") is V11() real ext-real Element of REAL
((L12 * ((R1 ^\ N2) . L11)) * (((R1 ^\ N2) . L11) ")) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . L11) is V11() real ext-real Element of REAL
((R1 ^\ N2) . L11) * (((R1 ^\ N2) . L11) ") is V11() real ext-real Element of REAL
L12 * (((R1 ^\ N2) . L11) * (((R1 ^\ N2) . L11) ")) is V11() real ext-real Element of REAL
(L12 * (((R1 ^\ N2) . L11) * (((R1 ^\ N2) . L11) "))) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . L11) is V11() real ext-real Element of REAL
(L12 * 1) + (((R2 /* (R1 ^\ N2)) (#) ((R1 ^\ N2) ")) . L11) is V11() real ext-real Element of REAL
N . L11 is V11() real ext-real Element of REAL
N is set
N is set
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
((R1 + x1) ^\ N2) . N is V11() real ext-real Element of REAL
(2,2,f,z0) . (((R1 + x1) ^\ N2) . N) is V11() real ext-real Element of REAL
(x1 ^\ N2) . N is V11() real ext-real Element of REAL
(2,2,f,z0) . ((x1 ^\ N2) . N) is V11() real ext-real Element of REAL
((2,2,f,z0) . (((R1 + x1) ^\ N2) . N)) - ((2,2,f,z0) . ((x1 ^\ N2) . N)) is V11() real ext-real Element of REAL
(R1 ^\ N2) . N is V11() real ext-real Element of REAL
L2 . ((R1 ^\ N2) . N) is V11() real ext-real Element of REAL
R2 . ((R1 ^\ N2) . N) is V11() real ext-real Element of REAL
(L2 . ((R1 ^\ N2) . N)) + (R2 . ((R1 ^\ N2) . N)) is V11() real ext-real Element of REAL
(((R1 + x1) ^\ N2) . N) - ((x1 ^\ N2) . N) is V11() real ext-real Element of REAL
(R1 ^\ N2) + (x1 ^\ N2) 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))
((R1 ^\ N2) + (x1 ^\ N2)) . N is V11() real ext-real Element of REAL
(((R1 ^\ N2) + (x1 ^\ N2)) . N) - ((x1 ^\ N2) . N) is V11() real ext-real Element of REAL
((R1 ^\ N2) . N) + ((x1 ^\ N2) . N) is V11() real ext-real Element of REAL
(((R1 ^\ N2) . N) + ((x1 ^\ N2) . N)) - ((x1 ^\ N2) . N) is V11() real ext-real Element of REAL
(2,2,f,z0) /* ((R1 + x1) ^\ N2) 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))
(2,2,f,z0) /* (x1 ^\ N2) 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))
((2,2,f,z0) /* ((R1 + x1) ^\ N2)) - ((2,2,f,z0) /* (x1 ^\ N2)) 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))
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V136() V159() V160() V161() V162() V163() V164() V165() Element of NAT
(((2,2,f,z0) /* ((R1 + x1) ^\ N2)) - ((2,2,f,z0) /* (x1 ^\ N2))) . N is V11() real ext-real Element of REAL
((2,2,f,z0) /* ((R1 + x1) ^\ N2)) . N is V11() real ext-real Element of REAL
((2,2,f,z0) /* (x1 ^\ N2)) . N is V11() real ext-real Element of REAL
(((2,2,f,z0) /* ((R1 + x1) ^\ N2)) . N) - (((2,2,f,z0) /* (x1 ^\ N2)) . N) is V11() real ext-real Element of REAL
((R1 + x1) ^\ N2) . N is V11() real ext-real Element of REAL
(2,2,f,z0) . (((R1 + x1) ^\ N2) . N) is V11() real ext-real Element of REAL
((2,2,f,z0) . (((R1 + x1) ^\ N2) . N)) - (((2,2,f,z0) /* (x1 ^\ N2)) . N) is V11() real ext-real Element of REAL
(x1 ^\ N2) . N is V11() real ext-real Element of REAL
(2,2,f,z0) . ((x1 ^\ N2) . N) is V11() real ext-real Element of REAL
((2,2,f,z0) . (((R1 + x1) ^\ N2) . N)) - ((2,2,f,z0) . ((x1 ^\ N2) . N)) is V11() real ext-real Element of REAL
(R1 ^\ N2) . N is V11() real ext-real Element of REAL
L2 . ((R1 ^\ N2) . N) is V11() real ext-real Element of REAL
R2 . ((R1 ^\ N2) . N) is V11() real ext-real Element of REAL
(L2 . ((R1 ^\ N2) . N)) + (R2 . ((R1 ^\ N2) . N)) is V11() real ext-real Element of REAL
(L2 /* (R1 ^\ N2)) . N is V11() real ext-real Element of REAL
((L2 /* (R1 ^\ N2)) . N) + (R2 . ((R1 ^\ N2) . N)) is V11() real ext-real Element of REAL
(R2 /* (R1 ^\ N2)) . N is V11() real ext-real Element of REAL
((L2 /* (R1 ^\ N2)) . N) + ((R2 /* (R1 ^\ N2)) . N) is V11() real ext-real Element of REAL
((L2 /* (R1 ^\ N2)) + (R2 /* (R1 ^\ N2))) . N is V11() real ext-real Element of REAL
((2,2,f,z0) /* (R1 + x1)) ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of (2,2,f,z0) /* (R1 + x1)
(((2,2,f,z0) /* (R1 + x1)) ^\ N2) - ((2,2,f,z0) /* (x1 ^\ N2)) 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))
((((2,2,f,z0) /* (R1 + x1)) ^\ N2) - ((2,2,f,z0) /* (x1 ^\ N2))) (#) ((R1 ^\ N2) ") 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))
((2,2,f,z0) /* x1) ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of (2,2,f,z0) /* x1
(((2,2,f,z0) /* (R1 + x1)) ^\ N2) - (((2,2,f,z0) /* x1) ^\ N2) 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))
((((2,2,f,z0) /* (R1 + x1)) ^\ N2) - (((2,2,f,z0) /* x1) ^\ N2)) (#) ((R1 ^\ N2) ") 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))
(((2,2,f,z0) /* (R1 + x1)) - ((2,2,f,z0) /* x1)) ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of ((2,2,f,z0) /* (R1 + x1)) - ((2,2,f,z0) /* x1)
((((2,2,f,z0) /* (R1 + x1)) - ((2,2,f,z0) /* x1)) ^\ N2) (#) ((R1 ^\ N2) ") 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))
(R1 ") ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of R1 "
((((2,2,f,z0) /* (R1 + x1)) - ((2,2,f,z0) /* x1)) ^\ N2) (#) ((R1 ") ^\ N2) 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))
(((2,2,f,z0) /* (R1 + x1)) - ((2,2,f,z0) /* x1)) (#) (R1 ") 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))
((((2,2,f,z0) /* (R1 + x1)) - ((2,2,f,z0) /* x1)) (#) (R1 ")) ^\ N2 is V1() V16() V19( NAT ) V20( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of (((2,2,f,z0) /* (R1 + x1)) - ((2,2,f,z0) /* x1)) (#) (R1 ")
N is V11() real ext-real Element of REAL
(2,2,f,z0) . N is V11() real ext-real Element of REAL
((2,2,f,z0) . N) - ((2,2,f,z0) . y0) is V11() real ext-real Element of REAL
N - y0 is V11() real ext-real Element of REAL
L2 . (N - y0) is V11() real ext-real Element of REAL
R2 . (N - y0) is V11() real ext-real Element of REAL
(L2 . (N - y0)) + (R2 . (N - y0)) is V11() real ext-real Element of REAL
f 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
z0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),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))
z0 (#) x0 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,z0,f) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (1,f) 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 * (reproj (1,f)) 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) is V160() V161() V162() Element of K6(REAL)
y0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*y0,y0*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set
(2,1,z0,f) . y0 is V11() real ext-real Element of REAL
N1 is V160() V161() V162() Neighbourhood of y0
L1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N1 is V160() V161() V162() Neighbourhood of y0
L1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R1 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 V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R1 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,x0,f) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
x0 * (reproj (1,f)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (2,1,x0,f) is V160() V161() V162() Element of K6(REAL)
x1 is V11() real ext-real Element of REAL
y1 is V11() real ext-real Element of REAL
<*x1,y1*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set
(2,1,x0,f) . x1 is V11() real ext-real Element of REAL
(2,1,x0,f) . y0 is V11() real ext-real Element of REAL
N2 is V160() V161() V162() Neighbourhood of x1
L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R2 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 V160() V161() V162() Neighbourhood of y0
L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V160() V161() V162() Neighbourhood of y0
(2,1,(z0 (#) x0),f) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(z0 (#) x0) * (reproj (1,f)) 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 (#) x0),f) is V160() V161() V162() Element of K6(REAL)
L12 is V11() real ext-real Element of REAL
(reproj (1,f)) . L12 is V61(2) FinSequence-like Element of REAL 2
dom z0 is functional FinSequence-membered Element of K6((REAL 2))
dom x0 is functional FinSequence-membered Element of K6((REAL 2))
(dom z0) /\ (dom x0) is functional FinSequence-membered Element of K6((REAL 2))
dom (z0 (#) x0) is functional FinSequence-membered Element of K6((REAL 2))
dom (reproj (1,f)) is V160() V161() V162() Element of K6(REAL)
L12 is set
((2,1,z0,f) . y0) (#) R2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((2,1,x0,f) . y0) (#) R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R1 (#) R2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R1 (#) L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R2 (#) L1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
L1 (#) L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R16 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 V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R16 + L is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R11 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R18 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R11 + R18 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R14 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,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 RestFunc-like Element of K6(K7(REAL,REAL))
L11 + L12 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((2,1,x0,f) . y0) (#) L1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((2,1,z0,f) . y0) (#) L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R15 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R17 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R15 + R17 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R13 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R13 + R14 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R20 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R12 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R20 + R12 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom ((z0 (#) x0) * (reproj (1,f))) is V160() V161() V162() Element of K6(REAL)
dom (reproj (1,f)) is V160() V161() V162() Element of K6(REAL)
(reproj (1,f)) . y0 is V61(2) FinSequence-like Element of REAL 2
dom (z0 (#) x0) is functional FinSequence-membered Element of K6((REAL 2))
dom z0 is functional FinSequence-membered Element of K6((REAL 2))
dom x0 is functional FinSequence-membered Element of K6((REAL 2))
(dom z0) /\ (dom x0) is functional FinSequence-membered Element of K6((REAL 2))
dom (z0 * (reproj (1,f))) is V160() V161() V162() Element of K6(REAL)
dom (x0 * (reproj (1,f))) is V160() V161() V162() Element of K6(REAL)
y is V11() real ext-real Element of REAL
(2,1,z0,f) . y is V11() real ext-real Element of REAL
((2,1,z0,f) . y) - ((2,1,z0,f) . y0) is V11() real ext-real Element of REAL
(((2,1,z0,f) . y) - ((2,1,z0,f) . y0)) + ((2,1,z0,f) . y0) is V11() real ext-real Element of REAL
y - y0 is V11() real ext-real Element of REAL
L1 . (y - y0) is V11() real ext-real Element of REAL
R1 . (y - y0) is V11() real ext-real Element of REAL
(L1 . (y - y0)) + (R1 . (y - y0)) is V11() real ext-real Element of REAL
((L1 . (y - y0)) + (R1 . (y - y0))) + ((2,1,z0,f) . y0) is V11() real ext-real Element of REAL
(reproj (1,f)) . y is V61(2) FinSequence-like Element of REAL 2
(2,1,(z0 (#) x0),f) . y is V11() real ext-real Element of REAL
(2,1,(z0 (#) x0),f) . y0 is V11() real ext-real Element of REAL
((2,1,(z0 (#) x0),f) . y) - ((2,1,(z0 (#) x0),f) . y0) is V11() real ext-real Element of REAL
(z0 (#) x0) . ((reproj (1,f)) . y) is V11() real ext-real Element of REAL
((z0 (#) x0) . ((reproj (1,f)) . y)) - ((2,1,(z0 (#) x0),f) . y0) is V11() real ext-real Element of REAL
z0 . ((reproj (1,f)) . y) is V11() real ext-real Element of REAL
x0 . ((reproj (1,f)) . y) is V11() real ext-real Element of REAL
(z0 . ((reproj (1,f)) . y)) * (x0 . ((reproj (1,f)) . y)) is V11() real ext-real Element of REAL
((z0 . ((reproj (1,f)) . y)) * (x0 . ((reproj (1,f)) . y))) - ((2,1,(z0 (#) x0),f) . y0) is V11() real ext-real Element of REAL
((2,1,z0,f) . y) * (x0 . ((reproj (1,f)) . y)) is V11() real ext-real Element of REAL
(((2,1,z0,f) . y) * (x0 . ((reproj (1,f)) . y))) - ((2,1,(z0 (#) x0),f) . y0) is V11() real ext-real Element of REAL
(2,1,x0,f) . y is V11() real ext-real Element of REAL
((2,1,z0,f) . y) * ((2,1,x0,f) . y) is V11() real ext-real Element of REAL
((z0 (#) x0) * (reproj (1,f))) . y0 is V11() real ext-real Element of REAL
(((2,1,z0,f) . y) * ((2,1,x0,f) . y)) - (((z0 (#) x0) * (reproj (1,f))) . y0) is V11() real ext-real Element of REAL
(z0 (#) x0) . ((reproj (1,f)) . y0) is V11() real ext-real Element of REAL
(((2,1,z0,f) . y) * ((2,1,x0,f) . y)) - ((z0 (#) x0) . ((reproj (1,f)) . y0)) is V11() real ext-real Element of REAL
z0 . ((reproj (1,f)) . y0) is V11() real ext-real Element of REAL
x0 . ((reproj (1,f)) . y0) is V11() real ext-real Element of REAL
(z0 . ((reproj (1,f)) . y0)) * (x0 . ((reproj (1,f)) . y0)) is V11() real ext-real Element of REAL
(((2,1,z0,f) . y) * ((2,1,x0,f) . y)) - ((z0 . ((reproj (1,f)) . y0)) * (x0 . ((reproj (1,f)) . y0))) is V11() real ext-real Element of REAL
((2,1,z0,f) . y0) * (x0 . ((reproj (1,f)) . y0)) is V11() real ext-real Element of REAL
(((2,1,z0,f) . y) * ((2,1,x0,f) . y)) - (((2,1,z0,f) . y0) * (x0 . ((reproj (1,f)) . y0))) is V11() real ext-real Element of REAL
((2,1,z0,f) . y) * ((2,1,x0,f) . y0) is V11() real ext-real Element of REAL
- (((2,1,z0,f) . y) * ((2,1,x0,f) . y0)) is V11() real ext-real Element of REAL
(((2,1,z0,f) . y) * ((2,1,x0,f) . y)) + (- (((2,1,z0,f) . y) * ((2,1,x0,f) . y0))) is V11() real ext-real Element of REAL
((((2,1,z0,f) . y) * ((2,1,x0,f) . y)) + (- (((2,1,z0,f) . y) * ((2,1,x0,f) . y0)))) + (((2,1,z0,f) . y) * ((2,1,x0,f) . y0)) is V11() real ext-real Element of REAL
((2,1,z0,f) . y0) * ((2,1,x0,f) . y0) is V11() real ext-real Element of REAL
(((((2,1,z0,f) . y) * ((2,1,x0,f) . y)) + (- (((2,1,z0,f) . y) * ((2,1,x0,f) . y0)))) + (((2,1,z0,f) . y) * ((2,1,x0,f) . y0))) - (((2,1,z0,f) . y0) * ((2,1,x0,f) . y0)) is V11() real ext-real Element of REAL
((2,1,x0,f) . y) - ((2,1,x0,f) . y0) is V11() real ext-real Element of REAL
((2,1,z0,f) . y) * (((2,1,x0,f) . y) - ((2,1,x0,f) . y0)) is V11() real ext-real Element of REAL
(((2,1,z0,f) . y) - ((2,1,z0,f) . y0)) * ((2,1,x0,f) . y0) is V11() real ext-real Element of REAL
(((2,1,z0,f) . y) * (((2,1,x0,f) . y) - ((2,1,x0,f) . y0))) + ((((2,1,z0,f) . y) - ((2,1,z0,f) . y0)) * ((2,1,x0,f) . y0)) is V11() real ext-real Element of REAL
((L1 . (y - y0)) + (R1 . (y - y0))) * ((2,1,x0,f) . y0) is V11() real ext-real Element of REAL
(((2,1,z0,f) . y) * (((2,1,x0,f) . y) - ((2,1,x0,f) . y0))) + (((L1 . (y - y0)) + (R1 . (y - y0))) * ((2,1,x0,f) . y0)) is V11() real ext-real Element of REAL
((2,1,x0,f) . y0) * (L1 . (y - y0)) is V11() real ext-real Element of REAL
((2,1,x0,f) . y0) * (R1 . (y - y0)) is V11() real ext-real Element of REAL
(((2,1,x0,f) . y0) * (L1 . (y - y0))) + (((2,1,x0,f) . y0) * (R1 . (y - y0))) is V11() real ext-real Element of REAL
(((2,1,z0,f) . y) * (((2,1,x0,f) . y) - ((2,1,x0,f) . y0))) + ((((2,1,x0,f) . y0) * (L1 . (y - y0))) + (((2,1,x0,f) . y0) * (R1 . (y - y0)))) is V11() real ext-real Element of REAL
R15 . (y - y0) is V11() real ext-real Element of REAL
(R15 . (y - y0)) + (((2,1,x0,f) . y0) * (R1 . (y - y0))) is V11() real ext-real Element of REAL
(((2,1,z0,f) . y) * (((2,1,x0,f) . y) - ((2,1,x0,f) . y0))) + ((R15 . (y - y0)) + (((2,1,x0,f) . y0) * (R1 . (y - y0)))) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) + ((2,1,z0,f) . y0)) * (((2,1,x0,f) . y) - ((2,1,x0,f) . y0)) is V11() real ext-real Element of REAL
L11 . (y - y0) is V11() real ext-real Element of REAL
(R15 . (y - y0)) + (L11 . (y - y0)) is V11() real ext-real Element of REAL
((((L1 . (y - y0)) + (R1 . (y - y0))) + ((2,1,z0,f) . y0)) * (((2,1,x0,f) . y) - ((2,1,x0,f) . y0))) + ((R15 . (y - y0)) + (L11 . (y - y0))) is V11() real ext-real Element of REAL
L2 . (y - y0) is V11() real ext-real Element of REAL
R2 . (y - y0) is V11() real ext-real Element of REAL
(L2 . (y - y0)) + (R2 . (y - y0)) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) + ((2,1,z0,f) . y0)) * ((L2 . (y - y0)) + (R2 . (y - y0))) is V11() real ext-real Element of REAL
((((L1 . (y - y0)) + (R1 . (y - y0))) + ((2,1,z0,f) . y0)) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((R15 . (y - y0)) + (L11 . (y - y0))) is V11() real ext-real Element of REAL
((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0))) is V11() real ext-real Element of REAL
((2,1,z0,f) . y0) * (L2 . (y - y0)) is V11() real ext-real Element of REAL
((2,1,z0,f) . y0) * (R2 . (y - y0)) is V11() real ext-real Element of REAL
(((2,1,z0,f) . y0) * (L2 . (y - y0))) + (((2,1,z0,f) . y0) * (R2 . (y - y0))) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((((2,1,z0,f) . y0) * (L2 . (y - y0))) + (((2,1,z0,f) . y0) * (R2 . (y - y0)))) is V11() real ext-real Element of REAL
((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((((2,1,z0,f) . y0) * (L2 . (y - y0))) + (((2,1,z0,f) . y0) * (R2 . (y - y0))))) + ((R15 . (y - y0)) + (L11 . (y - y0))) is V11() real ext-real Element of REAL
R17 . (y - y0) is V11() real ext-real Element of REAL
(R17 . (y - y0)) + (((2,1,z0,f) . y0) * (R2 . (y - y0))) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((R17 . (y - y0)) + (((2,1,z0,f) . y0) * (R2 . (y - y0)))) is V11() real ext-real Element of REAL
((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((R17 . (y - y0)) + (((2,1,z0,f) . y0) * (R2 . (y - y0))))) + ((R15 . (y - y0)) + (L11 . (y - y0))) is V11() real ext-real Element of REAL
L12 . (y - y0) is V11() real ext-real Element of REAL
(R17 . (y - y0)) + (L12 . (y - y0)) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((R17 . (y - y0)) + (L12 . (y - y0))) is V11() real ext-real Element of REAL
((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((R17 . (y - y0)) + (L12 . (y - y0)))) + ((R15 . (y - y0)) + (L11 . (y - y0))) is V11() real ext-real Element of REAL
(L11 . (y - y0)) + (L12 . (y - y0)) is V11() real ext-real Element of REAL
(R15 . (y - y0)) + ((L11 . (y - y0)) + (L12 . (y - y0))) is V11() real ext-real Element of REAL
(R17 . (y - y0)) + ((R15 . (y - y0)) + ((L11 . (y - y0)) + (L12 . (y - y0)))) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((R17 . (y - y0)) + ((R15 . (y - y0)) + ((L11 . (y - y0)) + (L12 . (y - y0))))) is V11() real ext-real Element of REAL
R13 . (y - y0) is V11() real ext-real Element of REAL
(R15 . (y - y0)) + (R13 . (y - y0)) is V11() real ext-real Element of REAL
(R17 . (y - y0)) + ((R15 . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((R17 . (y - y0)) + ((R15 . (y - y0)) + (R13 . (y - y0)))) is V11() real ext-real Element of REAL
(R15 . (y - y0)) + (R17 . (y - y0)) is V11() real ext-real Element of REAL
((R15 . (y - y0)) + (R17 . (y - y0))) + (R13 . (y - y0)) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + (((R15 . (y - y0)) + (R17 . (y - y0))) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
(L1 . (y - y0)) * (L2 . (y - y0)) is V11() real ext-real Element of REAL
(L1 . (y - y0)) * (R2 . (y - y0)) is V11() real ext-real Element of REAL
((L1 . (y - y0)) * (L2 . (y - y0))) + ((L1 . (y - y0)) * (R2 . (y - y0))) is V11() real ext-real Element of REAL
(R1 . (y - y0)) * ((L2 . (y - y0)) + (R2 . (y - y0))) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) * (L2 . (y - y0))) + ((L1 . (y - y0)) * (R2 . (y - y0)))) + ((R1 . (y - y0)) * ((L2 . (y - y0)) + (R2 . (y - y0)))) is V11() real ext-real Element of REAL
R19 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R19 . (y - y0) is V11() real ext-real Element of REAL
(R19 . (y - y0)) + (R13 . (y - y0)) is V11() real ext-real Element of REAL
((((L1 . (y - y0)) * (L2 . (y - y0))) + ((L1 . (y - y0)) * (R2 . (y - y0)))) + ((R1 . (y - y0)) * ((L2 . (y - y0)) + (R2 . (y - y0))))) + ((R19 . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
R14 . (y - y0) is V11() real ext-real Element of REAL
(R2 . (y - y0)) * (L1 . (y - y0)) is V11() real ext-real Element of REAL
(R14 . (y - y0)) + ((R2 . (y - y0)) * (L1 . (y - y0))) is V11() real ext-real Element of REAL
((R14 . (y - y0)) + ((R2 . (y - y0)) * (L1 . (y - y0)))) + ((R1 . (y - y0)) * ((L2 . (y - y0)) + (R2 . (y - y0)))) is V11() real ext-real Element of REAL
(((R14 . (y - y0)) + ((R2 . (y - y0)) * (L1 . (y - y0)))) + ((R1 . (y - y0)) * ((L2 . (y - y0)) + (R2 . (y - y0))))) + ((R19 . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
R18 . (y - y0) is V11() real ext-real Element of REAL
(R14 . (y - y0)) + (R18 . (y - y0)) is V11() real ext-real Element of REAL
(R1 . (y - y0)) * (L2 . (y - y0)) is V11() real ext-real Element of REAL
(R1 . (y - y0)) * (R2 . (y - y0)) is V11() real ext-real Element of REAL
((R1 . (y - y0)) * (L2 . (y - y0))) + ((R1 . (y - y0)) * (R2 . (y - y0))) is V11() real ext-real Element of REAL
((R14 . (y - y0)) + (R18 . (y - y0))) + (((R1 . (y - y0)) * (L2 . (y - y0))) + ((R1 . (y - y0)) * (R2 . (y - y0)))) is V11() real ext-real Element of REAL
(((R14 . (y - y0)) + (R18 . (y - y0))) + (((R1 . (y - y0)) * (L2 . (y - y0))) + ((R1 . (y - y0)) * (R2 . (y - y0))))) + ((R19 . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
R16 . (y - y0) is V11() real ext-real Element of REAL
(R16 . (y - y0)) + ((R1 . (y - y0)) * (R2 . (y - y0))) is V11() real ext-real Element of REAL
((R14 . (y - y0)) + (R18 . (y - y0))) + ((R16 . (y - y0)) + ((R1 . (y - y0)) * (R2 . (y - y0)))) is V11() real ext-real Element of REAL
(((R14 . (y - y0)) + (R18 . (y - y0))) + ((R16 . (y - y0)) + ((R1 . (y - y0)) * (R2 . (y - y0))))) + ((R19 . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
L . (y - y0) is V11() real ext-real Element of REAL
(R16 . (y - y0)) + (L . (y - y0)) is V11() real ext-real Element of REAL
((R14 . (y - y0)) + (R18 . (y - y0))) + ((R16 . (y - y0)) + (L . (y - y0))) is V11() real ext-real Element of REAL
(((R14 . (y - y0)) + (R18 . (y - y0))) + ((R16 . (y - y0)) + (L . (y - y0)))) + ((R19 . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
R11 . (y - y0) is V11() real ext-real Element of REAL
((R14 . (y - y0)) + (R18 . (y - y0))) + (R11 . (y - y0)) is V11() real ext-real Element of REAL
(((R14 . (y - y0)) + (R18 . (y - y0))) + (R11 . (y - y0))) + ((R19 . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
(R11 . (y - y0)) + (R18 . (y - y0)) is V11() real ext-real Element of REAL
(R14 . (y - y0)) + ((R11 . (y - y0)) + (R18 . (y - y0))) is V11() real ext-real Element of REAL
((R14 . (y - y0)) + ((R11 . (y - y0)) + (R18 . (y - y0)))) + ((R19 . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
R12 . (y - y0) is V11() real ext-real Element of REAL
(R14 . (y - y0)) + (R12 . (y - y0)) is V11() real ext-real Element of REAL
((R19 . (y - y0)) + (R13 . (y - y0))) + ((R14 . (y - y0)) + (R12 . (y - y0))) is V11() real ext-real Element of REAL
(R13 . (y - y0)) + (R14 . (y - y0)) is V11() real ext-real Element of REAL
((R13 . (y - y0)) + (R14 . (y - y0))) + (R12 . (y - y0)) is V11() real ext-real Element of REAL
(R19 . (y - y0)) + (((R13 . (y - y0)) + (R14 . (y - y0))) + (R12 . (y - y0))) is V11() real ext-real Element of REAL
R20 . (y - y0) is V11() real ext-real Element of REAL
(R20 . (y - y0)) + (R12 . (y - y0)) is V11() real ext-real Element of REAL
(R19 . (y - y0)) + ((R20 . (y - y0)) + (R12 . (y - y0))) is V11() real ext-real Element of REAL
R is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R . (y - y0) is V11() real ext-real Element of REAL
(R19 . (y - y0)) + (R . (y - y0)) is V11() real ext-real Element of REAL
f 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
z0 is V16() V19( REAL 2) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7((REAL 2),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))
z0 (#) x0 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,z0,f) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
reproj (2,f) 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 * (reproj (2,f)) 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) is V160() V161() V162() Element of K6(REAL)
y0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*y0,y0*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set
(2,2,z0,f) . y0 is V11() real ext-real Element of REAL
N1 is V160() V161() V162() Neighbourhood of y0
L1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N1 is V160() V161() V162() Neighbourhood of y0
L1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R1 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 V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R1 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,x0,f) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
x0 * (reproj (2,f)) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (2,2,x0,f) is V160() V161() V162() Element of K6(REAL)
x1 is V11() real ext-real Element of REAL
y1 is V11() real ext-real Element of REAL
<*x1,y1*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set
(2,2,x0,f) . y1 is V11() real ext-real Element of REAL
(2,2,x0,f) . y0 is V11() real ext-real Element of REAL
N2 is V160() V161() V162() Neighbourhood of y1
L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R2 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 V160() V161() V162() Neighbourhood of y0
L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
N is V160() V161() V162() Neighbourhood of y0
(2,2,(z0 (#) x0),f) is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(z0 (#) x0) * (reproj (2,f)) 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 (#) x0),f) is V160() V161() V162() Element of K6(REAL)
L12 is V11() real ext-real Element of REAL
(reproj (2,f)) . L12 is V61(2) FinSequence-like Element of REAL 2
dom z0 is functional FinSequence-membered Element of K6((REAL 2))
dom x0 is functional FinSequence-membered Element of K6((REAL 2))
(dom z0) /\ (dom x0) is functional FinSequence-membered Element of K6((REAL 2))
dom (z0 (#) x0) is functional FinSequence-membered Element of K6((REAL 2))
dom (reproj (2,f)) is V160() V161() V162() Element of K6(REAL)
L12 is set
((2,2,z0,f) . y0) (#) L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((2,2,x0,f) . y0) (#) L1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
L11 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear 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))
L11 + L12 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R1 (#) L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R2 (#) L1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
L1 (#) L2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((2,2,x0,f) . y0) (#) R1 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((2,2,z0,f) . y0) (#) R2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R11 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R12 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R11 + R12 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R13 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R14 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R13 + R14 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R1 (#) R2 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R16 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R17 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R16 + R17 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R19 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R18 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R19 + R18 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R15 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R20 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R15 + R20 is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom ((z0 (#) x0) * (reproj (2,f))) is V160() V161() V162() Element of K6(REAL)
dom (reproj (2,f)) is V160() V161() V162() Element of K6(REAL)
(reproj (2,f)) . y0 is V61(2) FinSequence-like Element of REAL 2
dom (z0 (#) x0) is functional FinSequence-membered Element of K6((REAL 2))
dom z0 is functional FinSequence-membered Element of K6((REAL 2))
dom x0 is functional FinSequence-membered Element of K6((REAL 2))
(dom z0) /\ (dom x0) is functional FinSequence-membered Element of K6((REAL 2))
dom (z0 * (reproj (2,f))) is V160() V161() V162() Element of K6(REAL)
dom (x0 * (reproj (2,f))) is V160() V161() V162() Element of K6(REAL)
y is V11() real ext-real Element of REAL
(2,2,z0,f) . y is V11() real ext-real Element of REAL
((2,2,z0,f) . y) - ((2,2,z0,f) . y0) is V11() real ext-real Element of REAL
(((2,2,z0,f) . y) - ((2,2,z0,f) . y0)) + ((2,2,z0,f) . y0) is V11() real ext-real Element of REAL
y - y0 is V11() real ext-real Element of REAL
L1 . (y - y0) is V11() real ext-real Element of REAL
R1 . (y - y0) is V11() real ext-real Element of REAL
(L1 . (y - y0)) + (R1 . (y - y0)) is V11() real ext-real Element of REAL
((L1 . (y - y0)) + (R1 . (y - y0))) + ((2,2,z0,f) . y0) is V11() real ext-real Element of REAL
(reproj (2,f)) . y is V61(2) FinSequence-like Element of REAL 2
(2,2,(z0 (#) x0),f) . y is V11() real ext-real Element of REAL
(2,2,(z0 (#) x0),f) . y0 is V11() real ext-real Element of REAL
((2,2,(z0 (#) x0),f) . y) - ((2,2,(z0 (#) x0),f) . y0) is V11() real ext-real Element of REAL
(z0 (#) x0) . ((reproj (2,f)) . y) is V11() real ext-real Element of REAL
((z0 (#) x0) . ((reproj (2,f)) . y)) - ((2,2,(z0 (#) x0),f) . y0) is V11() real ext-real Element of REAL
z0 . ((reproj (2,f)) . y) is V11() real ext-real Element of REAL
x0 . ((reproj (2,f)) . y) is V11() real ext-real Element of REAL
(z0 . ((reproj (2,f)) . y)) * (x0 . ((reproj (2,f)) . y)) is V11() real ext-real Element of REAL
((z0 . ((reproj (2,f)) . y)) * (x0 . ((reproj (2,f)) . y))) - ((2,2,(z0 (#) x0),f) . y0) is V11() real ext-real Element of REAL
((2,2,z0,f) . y) * (x0 . ((reproj (2,f)) . y)) is V11() real ext-real Element of REAL
(((2,2,z0,f) . y) * (x0 . ((reproj (2,f)) . y))) - ((2,2,(z0 (#) x0),f) . y0) is V11() real ext-real Element of REAL
(2,2,x0,f) . y is V11() real ext-real Element of REAL
((2,2,z0,f) . y) * ((2,2,x0,f) . y) is V11() real ext-real Element of REAL
((z0 (#) x0) * (reproj (2,f))) . y0 is V11() real ext-real Element of REAL
(((2,2,z0,f) . y) * ((2,2,x0,f) . y)) - (((z0 (#) x0) * (reproj (2,f))) . y0) is V11() real ext-real Element of REAL
(z0 (#) x0) . ((reproj (2,f)) . y0) is V11() real ext-real Element of REAL
(((2,2,z0,f) . y) * ((2,2,x0,f) . y)) - ((z0 (#) x0) . ((reproj (2,f)) . y0)) is V11() real ext-real Element of REAL
z0 . ((reproj (2,f)) . y0) is V11() real ext-real Element of REAL
x0 . ((reproj (2,f)) . y0) is V11() real ext-real Element of REAL
(z0 . ((reproj (2,f)) . y0)) * (x0 . ((reproj (2,f)) . y0)) is V11() real ext-real Element of REAL
(((2,2,z0,f) . y) * ((2,2,x0,f) . y)) - ((z0 . ((reproj (2,f)) . y0)) * (x0 . ((reproj (2,f)) . y0))) is V11() real ext-real Element of REAL
((2,2,z0,f) . y0) * (x0 . ((reproj (2,f)) . y0)) is V11() real ext-real Element of REAL
(((2,2,z0,f) . y) * ((2,2,x0,f) . y)) - (((2,2,z0,f) . y0) * (x0 . ((reproj (2,f)) . y0))) is V11() real ext-real Element of REAL
((2,2,z0,f) . y) * ((2,2,x0,f) . y0) is V11() real ext-real Element of REAL
- (((2,2,z0,f) . y) * ((2,2,x0,f) . y0)) is V11() real ext-real Element of REAL
(((2,2,z0,f) . y) * ((2,2,x0,f) . y)) + (- (((2,2,z0,f) . y) * ((2,2,x0,f) . y0))) is V11() real ext-real Element of REAL
((((2,2,z0,f) . y) * ((2,2,x0,f) . y)) + (- (((2,2,z0,f) . y) * ((2,2,x0,f) . y0)))) + (((2,2,z0,f) . y) * ((2,2,x0,f) . y0)) is V11() real ext-real Element of REAL
((2,2,z0,f) . y0) * ((2,2,x0,f) . y0) is V11() real ext-real Element of REAL
(((((2,2,z0,f) . y) * ((2,2,x0,f) . y)) + (- (((2,2,z0,f) . y) * ((2,2,x0,f) . y0)))) + (((2,2,z0,f) . y) * ((2,2,x0,f) . y0))) - (((2,2,z0,f) . y0) * ((2,2,x0,f) . y0)) is V11() real ext-real Element of REAL
((2,2,x0,f) . y) - ((2,2,x0,f) . y0) is V11() real ext-real Element of REAL
((2,2,z0,f) . y) * (((2,2,x0,f) . y) - ((2,2,x0,f) . y0)) is V11() real ext-real Element of REAL
(((2,2,z0,f) . y) - ((2,2,z0,f) . y0)) * ((2,2,x0,f) . y0) is V11() real ext-real Element of REAL
(((2,2,z0,f) . y) * (((2,2,x0,f) . y) - ((2,2,x0,f) . y0))) + ((((2,2,z0,f) . y) - ((2,2,z0,f) . y0)) * ((2,2,x0,f) . y0)) is V11() real ext-real Element of REAL
((L1 . (y - y0)) + (R1 . (y - y0))) * ((2,2,x0,f) . y0) is V11() real ext-real Element of REAL
(((2,2,z0,f) . y) * (((2,2,x0,f) . y) - ((2,2,x0,f) . y0))) + (((L1 . (y - y0)) + (R1 . (y - y0))) * ((2,2,x0,f) . y0)) is V11() real ext-real Element of REAL
((2,2,x0,f) . y0) * (L1 . (y - y0)) is V11() real ext-real Element of REAL
((2,2,x0,f) . y0) * (R1 . (y - y0)) is V11() real ext-real Element of REAL
(((2,2,x0,f) . y0) * (L1 . (y - y0))) + (((2,2,x0,f) . y0) * (R1 . (y - y0))) is V11() real ext-real Element of REAL
(((2,2,z0,f) . y) * (((2,2,x0,f) . y) - ((2,2,x0,f) . y0))) + ((((2,2,x0,f) . y0) * (L1 . (y - y0))) + (((2,2,x0,f) . y0) * (R1 . (y - y0)))) is V11() real ext-real Element of REAL
L11 . (y - y0) is V11() real ext-real Element of REAL
(L11 . (y - y0)) + (((2,2,x0,f) . y0) * (R1 . (y - y0))) is V11() real ext-real Element of REAL
(((2,2,z0,f) . y) * (((2,2,x0,f) . y) - ((2,2,x0,f) . y0))) + ((L11 . (y - y0)) + (((2,2,x0,f) . y0) * (R1 . (y - y0)))) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) + ((2,2,z0,f) . y0)) * (((2,2,x0,f) . y) - ((2,2,x0,f) . y0)) is V11() real ext-real Element of REAL
R11 . (y - y0) is V11() real ext-real Element of REAL
(L11 . (y - y0)) + (R11 . (y - y0)) is V11() real ext-real Element of REAL
((((L1 . (y - y0)) + (R1 . (y - y0))) + ((2,2,z0,f) . y0)) * (((2,2,x0,f) . y) - ((2,2,x0,f) . y0))) + ((L11 . (y - y0)) + (R11 . (y - y0))) is V11() real ext-real Element of REAL
L2 . (y - y0) is V11() real ext-real Element of REAL
R2 . (y - y0) is V11() real ext-real Element of REAL
(L2 . (y - y0)) + (R2 . (y - y0)) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) + ((2,2,z0,f) . y0)) * ((L2 . (y - y0)) + (R2 . (y - y0))) is V11() real ext-real Element of REAL
((((L1 . (y - y0)) + (R1 . (y - y0))) + ((2,2,z0,f) . y0)) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L11 . (y - y0)) + (R11 . (y - y0))) is V11() real ext-real Element of REAL
((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0))) is V11() real ext-real Element of REAL
((2,2,z0,f) . y0) * (L2 . (y - y0)) is V11() real ext-real Element of REAL
((2,2,z0,f) . y0) * (R2 . (y - y0)) is V11() real ext-real Element of REAL
(((2,2,z0,f) . y0) * (L2 . (y - y0))) + (((2,2,z0,f) . y0) * (R2 . (y - y0))) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((((2,2,z0,f) . y0) * (L2 . (y - y0))) + (((2,2,z0,f) . y0) * (R2 . (y - y0)))) is V11() real ext-real Element of REAL
((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((((2,2,z0,f) . y0) * (L2 . (y - y0))) + (((2,2,z0,f) . y0) * (R2 . (y - y0))))) + ((L11 . (y - y0)) + (R11 . (y - y0))) is V11() real ext-real Element of REAL
L12 . (y - y0) is V11() real ext-real Element of REAL
(L12 . (y - y0)) + (((2,2,z0,f) . y0) * (R2 . (y - y0))) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + (((2,2,z0,f) . y0) * (R2 . (y - y0)))) is V11() real ext-real Element of REAL
((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + (((2,2,z0,f) . y0) * (R2 . (y - y0))))) + ((L11 . (y - y0)) + (R11 . (y - y0))) is V11() real ext-real Element of REAL
R12 . (y - y0) is V11() real ext-real Element of REAL
(L12 . (y - y0)) + (R12 . (y - y0)) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + (R12 . (y - y0))) is V11() real ext-real Element of REAL
((((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + (R12 . (y - y0)))) + ((L11 . (y - y0)) + (R11 . (y - y0))) is V11() real ext-real Element of REAL
(R11 . (y - y0)) + (R12 . (y - y0)) is V11() real ext-real Element of REAL
(L11 . (y - y0)) + ((R11 . (y - y0)) + (R12 . (y - y0))) is V11() real ext-real Element of REAL
(L12 . (y - y0)) + ((L11 . (y - y0)) + ((R11 . (y - y0)) + (R12 . (y - y0)))) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + ((L11 . (y - y0)) + ((R11 . (y - y0)) + (R12 . (y - y0))))) is V11() real ext-real Element of REAL
R13 . (y - y0) is V11() real ext-real Element of REAL
(L11 . (y - y0)) + (R13 . (y - y0)) is V11() real ext-real Element of REAL
(L12 . (y - y0)) + ((L11 . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + ((L12 . (y - y0)) + ((L11 . (y - y0)) + (R13 . (y - y0)))) is V11() real ext-real Element of REAL
(L11 . (y - y0)) + (L12 . (y - y0)) is V11() real ext-real Element of REAL
((L11 . (y - y0)) + (L12 . (y - y0))) + (R13 . (y - y0)) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) + (R1 . (y - y0))) * ((L2 . (y - y0)) + (R2 . (y - y0)))) + (((L11 . (y - y0)) + (L12 . (y - y0))) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
(L1 . (y - y0)) * (L2 . (y - y0)) is V11() real ext-real Element of REAL
(L1 . (y - y0)) * (R2 . (y - y0)) is V11() real ext-real Element of REAL
((L1 . (y - y0)) * (L2 . (y - y0))) + ((L1 . (y - y0)) * (R2 . (y - y0))) is V11() real ext-real Element of REAL
(R1 . (y - y0)) * ((L2 . (y - y0)) + (R2 . (y - y0))) is V11() real ext-real Element of REAL
(((L1 . (y - y0)) * (L2 . (y - y0))) + ((L1 . (y - y0)) * (R2 . (y - y0)))) + ((R1 . (y - y0)) * ((L2 . (y - y0)) + (R2 . (y - y0)))) is V11() real ext-real Element of REAL
L is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . (y - y0) is V11() real ext-real Element of REAL
(L . (y - y0)) + (R13 . (y - y0)) is V11() real ext-real Element of REAL
((((L1 . (y - y0)) * (L2 . (y - y0))) + ((L1 . (y - y0)) * (R2 . (y - y0)))) + ((R1 . (y - y0)) * ((L2 . (y - y0)) + (R2 . (y - y0))))) + ((L . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
R14 . (y - y0) is V11() real ext-real Element of REAL
(R2 . (y - y0)) * (L1 . (y - y0)) is V11() real ext-real Element of REAL
(R14 . (y - y0)) + ((R2 . (y - y0)) * (L1 . (y - y0))) is V11() real ext-real Element of REAL
((R14 . (y - y0)) + ((R2 . (y - y0)) * (L1 . (y - y0)))) + ((R1 . (y - y0)) * ((L2 . (y - y0)) + (R2 . (y - y0)))) is V11() real ext-real Element of REAL
(((R14 . (y - y0)) + ((R2 . (y - y0)) * (L1 . (y - y0)))) + ((R1 . (y - y0)) * ((L2 . (y - y0)) + (R2 . (y - y0))))) + ((L . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
R18 . (y - y0) is V11() real ext-real Element of REAL
(R14 . (y - y0)) + (R18 . (y - y0)) is V11() real ext-real Element of REAL
(R1 . (y - y0)) * (L2 . (y - y0)) is V11() real ext-real Element of REAL
(R1 . (y - y0)) * (R2 . (y - y0)) is V11() real ext-real Element of REAL
((R1 . (y - y0)) * (L2 . (y - y0))) + ((R1 . (y - y0)) * (R2 . (y - y0))) is V11() real ext-real Element of REAL
((R14 . (y - y0)) + (R18 . (y - y0))) + (((R1 . (y - y0)) * (L2 . (y - y0))) + ((R1 . (y - y0)) * (R2 . (y - y0)))) is V11() real ext-real Element of REAL
(((R14 . (y - y0)) + (R18 . (y - y0))) + (((R1 . (y - y0)) * (L2 . (y - y0))) + ((R1 . (y - y0)) * (R2 . (y - y0))))) + ((L . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
R16 . (y - y0) is V11() real ext-real Element of REAL
(R16 . (y - y0)) + ((R1 . (y - y0)) * (R2 . (y - y0))) is V11() real ext-real Element of REAL
((R14 . (y - y0)) + (R18 . (y - y0))) + ((R16 . (y - y0)) + ((R1 . (y - y0)) * (R2 . (y - y0)))) is V11() real ext-real Element of REAL
(((R14 . (y - y0)) + (R18 . (y - y0))) + ((R16 . (y - y0)) + ((R1 . (y - y0)) * (R2 . (y - y0))))) + ((L . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
R17 . (y - y0) is V11() real ext-real Element of REAL
(R16 . (y - y0)) + (R17 . (y - y0)) is V11() real ext-real Element of REAL
((R14 . (y - y0)) + (R18 . (y - y0))) + ((R16 . (y - y0)) + (R17 . (y - y0))) is V11() real ext-real Element of REAL
(((R14 . (y - y0)) + (R18 . (y - y0))) + ((R16 . (y - y0)) + (R17 . (y - y0)))) + ((L . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
R19 . (y - y0) is V11() real ext-real Element of REAL
((R14 . (y - y0)) + (R18 . (y - y0))) + (R19 . (y - y0)) is V11() real ext-real Element of REAL
(((R14 . (y - y0)) + (R18 . (y - y0))) + (R19 . (y - y0))) + ((L . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
(R19 . (y - y0)) + (R18 . (y - y0)) is V11() real ext-real Element of REAL
(R14 . (y - y0)) + ((R19 . (y - y0)) + (R18 . (y - y0))) is V11() real ext-real Element of REAL
((R14 . (y - y0)) + ((R19 . (y - y0)) + (R18 . (y - y0)))) + ((L . (y - y0)) + (R13 . (y - y0))) is V11() real ext-real Element of REAL
R20 . (y - y0) is V11() real ext-real Element of REAL
(R14 . (y - y0)) + (R20 . (y - y0)) is V11() real ext-real Element of REAL
((L . (y - y0)) + (R13 . (y - y0))) + ((R14 . (y - y0)) + (R20 . (y - y0))) is V11() real ext-real Element of REAL
(R13 . (y - y0)) + (R14 . (y - y0)) is V11() real ext-real Element of REAL
((R13 . (y - y0)) + (R14 . (y - y0))) + (R20 . (y - y0)) is V11() real ext-real Element of REAL
(L . (y - y0)) + (((R13 . (y - y0)) + (R14 . (y - y0))) + (R20 . (y - y0))) is V11() real ext-real Element of REAL
R15 . (y - y0) is V11() real ext-real Element of REAL
(R15 . (y - y0)) + (R20 . (y - y0)) is V11() real ext-real Element of REAL
(L . (y - y0)) + ((R15 . (y - y0)) + (R20 . (y - y0))) is V11() real ext-real Element of REAL
R is V16() V19( REAL ) V20( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
R . (y - y0) is V11() real ext-real Element of REAL
(L . (y - y0)) + (R . (y - 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
(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))
(proj (1,2)) . z0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is 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,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))
(proj (2,2)) . z0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
y0 is V11() real ext-real Element of REAL
<*x0,y0*> is V1() V16() V19( NAT ) Function-like V54() V61(2) FinSequence-like FinSubsequence-like set