REAL is non zero V33() V166() V167() V168() V172() set
NAT is non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non zero V33() V166() V172() set
K6(COMPLEX) is set
omega is non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() set
K6(omega) is set
K6(NAT) is set
K7(NAT,REAL) is complex-yielding V115() V116() set
K6(K7(NAT,REAL)) is set
K190() is non zero set
K7(K190(),K190()) is set
K7(K7(K190(),K190()),K190()) is set
K6(K7(K7(K190(),K190()),K190())) is set
K7(REAL,K190()) is set
K7(K7(REAL,K190()),K190()) is set
K6(K7(K7(REAL,K190()),K190())) is set
K196() is L12()
the carrier of K196() is set
K6( the carrier of K196()) is set
K200() is Element of K6( the carrier of K196())
K7(K200(),K200()) is set
K7(K7(K200(),K200()),REAL) is complex-yielding V115() V116() set
K6(K7(K7(K200(),K200()),REAL)) is set
K203() is Element of K6( the carrier of K196())
K7(K203(),REAL) is complex-yielding V115() V116() set
K6(K7(K203(),REAL)) is set
RAT is non zero V33() V166() V167() V168() V169() V172() set
INT is non zero V33() V166() V167() V168() V169() V170() V172() set
K7(COMPLEX,COMPLEX) is complex-yielding set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-yielding set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is complex-yielding V115() V116() set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is complex-yielding V115() V116() set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is RAT -valued complex-yielding V115() V116() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is RAT -valued complex-yielding V115() V116() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is RAT -valued INT -valued complex-yielding V115() V116() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is RAT -valued INT -valued complex-yielding V115() V116() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is RAT -valued INT -valued complex-yielding V115() V116() V117() set
K7(K7(NAT,NAT),NAT) is RAT -valued INT -valued complex-yielding V115() V116() V117() set
K6(K7(K7(NAT,NAT),NAT)) is set
1 is non zero epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V126() V127() V166() V167() V168() V169() V170() V171() Element of NAT
K7(1,1) is RAT -valued INT -valued complex-yielding V115() V116() V117() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is RAT -valued INT -valued complex-yielding V115() V116() V117() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is complex-yielding V115() V116() set
K6(K7(K7(1,1),REAL)) is set
2 is non zero epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V126() V127() V166() V167() V168() V169() V170() V171() Element of NAT
K7(2,2) is RAT -valued INT -valued complex-yielding V115() V116() V117() set
K7(K7(2,2),REAL) is complex-yielding V115() V116() set
K6(K7(K7(2,2),REAL)) is set
TOP-REAL 2 is V45() V71() V96() V97() V98() V99() V100() V101() V102() TopSpace-like V208() L20()
the carrier of (TOP-REAL 2) is non zero set
REAL 1 is non zero FinSequence-membered M14( REAL )
K434(1,REAL) is FinSequence-membered M14( REAL )
K7((REAL 1),(REAL 1)) is set
K6(K7((REAL 1),(REAL 1))) is set
REAL-NS 1 is V45() V50() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() strict RealNormSpace-like V163() NORMSTR
the carrier of (REAL-NS 1) is non zero V2() set
R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) is V45() NORMSTR
BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) is Element of K6( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))))
R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1)) is V45() V71() V96() V97() V98() V99() V100() V101() V102() L12()
LinearOperators ((REAL-NS 1),(REAL-NS 1)) is Element of K6( the carrier of K350( the carrier of (REAL-NS 1),(REAL-NS 1)))
K350( the carrier of (REAL-NS 1),(REAL-NS 1)) is V45() V71() V96() V97() V98() V99() V100() V101() V102() L12()
Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) is non zero functional FUNCTION_DOMAIN of the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)
FuncZero ( the carrier of (REAL-NS 1),(REAL-NS 1)) is Relation-like the carrier of (REAL-NS 1) -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))
0. (REAL-NS 1) is zero Element of the carrier of (REAL-NS 1)
K285( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1),(0. (REAL-NS 1))) is non zero Relation-like the carrier of (REAL-NS 1) -defined the carrier of (REAL-NS 1) -valued Function-like total quasi_total Element of K6(K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))
K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) is set
K6(K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) is set
FuncAdd ( the carrier of (REAL-NS 1),(REAL-NS 1)) is Relation-like K7((Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) -defined Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) -valued Function-like total quasi_total Element of K6(K7(K7((Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))))
K7((Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) is set
K7(K7((Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) is set
K6(K7(K7((Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))))) is set
FuncExtMult ( the carrier of (REAL-NS 1),(REAL-NS 1)) is Relation-like K7(REAL,(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) -defined Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) -valued Function-like total quasi_total Element of K6(K7(K7(REAL,(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))))
K7(REAL,(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) is set
K7(K7(REAL,(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) is set
K6(K7(K7(REAL,(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))))) is set
G12((Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),(FuncZero ( the carrier of (REAL-NS 1),(REAL-NS 1))),(FuncAdd ( the carrier of (REAL-NS 1),(REAL-NS 1))),(FuncExtMult ( the carrier of (REAL-NS 1),(REAL-NS 1)))) is strict L12()
the carrier of K350( the carrier of (REAL-NS 1),(REAL-NS 1)) is non zero set
K6( the carrier of K350( the carrier of (REAL-NS 1),(REAL-NS 1))) is set
K199(K350( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Element of LinearOperators ((REAL-NS 1),(REAL-NS 1))
K197(K350( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Relation-like K7((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) -defined LinearOperators ((REAL-NS 1),(REAL-NS 1)) -valued Function-like quasi_total Element of K6(K7(K7((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))))
K7((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K7(K7((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K6(K7(K7((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1))))) is set
K198(K350( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Relation-like K7(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) -defined LinearOperators ((REAL-NS 1),(REAL-NS 1)) -valued Function-like quasi_total Element of K6(K7(K7(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))))
K7(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K7(K7(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K6(K7(K7(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1))))) is set
G12((LinearOperators ((REAL-NS 1),(REAL-NS 1))),K199(K350( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),K197(K350( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),K198(K350( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1))))) is strict L12()
the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))) is non zero set
K6( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K199((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Element of BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))
K197((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Relation-like K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) -defined BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) -valued Function-like quasi_total Element of K6(K7(K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))))
K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K7(K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K6(K7(K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))))) is set
K198((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Relation-like K7(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) -defined BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) -valued Function-like quasi_total Element of K6(K7(K7(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))))
K7(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K7(K7(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K6(K7(K7(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))))) is set
BoundedLinearOperatorsNorm ((REAL-NS 1),(REAL-NS 1)) is Relation-like BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),REAL))
K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),REAL) is complex-yielding V115() V116() set
K6(K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),REAL)) is set
NORMSTR(# (BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),K199((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),K197((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),K198((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperatorsNorm ((REAL-NS 1),(REAL-NS 1))) #) is strict NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) is non zero set
K7(NAT,COMPLEX) is complex-yielding set
K6(K7(NAT,COMPLEX)) is set
0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V166() V167() V168() V169() V170() V171() V172() set
0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V126() V127() V166() V167() V168() V169() V170() V171() V172() Element of NAT
0. (TOP-REAL 2) is V40(2) FinSequence-like zero V116() Element of the carrier of (TOP-REAL 2)
|[0,0]| is V40(2) FinSequence-like V116() Element of the carrier of (TOP-REAL 2)
K7(2,REAL) is complex-yielding V115() V116() set
K6(K7(2,REAL)) is set
Re 0 is V11() real ext-real Element of REAL
Im 0 is V11() real ext-real Element of REAL
<i> is V11() Element of COMPLEX
Re <i> is V11() real ext-real Element of REAL
Im <i> is V11() real ext-real Element of REAL
|.<i>.| is V11() real ext-real Element of REAL
(Re <i>) ^2 is V11() real ext-real Element of REAL
(Im <i>) ^2 is V11() real ext-real Element of REAL
((Re <i>) ^2) + ((Im <i>) ^2) is V11() real ext-real Element of REAL
sqrt (((Re <i>) ^2) + ((Im <i>) ^2)) is V11() real ext-real Element of REAL
Seg 1 is V166() V167() V168() V169() V170() V171() Element of K6(NAT)
addreal is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(K7(REAL,REAL),REAL))
diffreal is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(K7(REAL,REAL),REAL))
1r is V11() Element of COMPLEX
proj (1,1) is non zero Relation-like REAL 1 -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7((REAL 1),REAL))
K7((REAL 1),REAL) is complex-yielding V115() V116() set
K6(K7((REAL 1),REAL)) is set
(proj (1,1)) " is Relation-like Function-like set
K7(REAL,(REAL 1)) is set
K6(K7(REAL,(REAL 1))) is set
dom ((proj (1,1)) ") is set
rng ((proj (1,1)) ") is set
0c is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V166() V167() V168() V169() V170() V171() V172() Element of COMPLEX
f is non zero Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(NAT,REAL))
lim f is V11() real ext-real Element of REAL
u is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
lim u is V11() Element of COMPLEX
v is V11() real ext-real set
z0 is V11() Element of COMPLEX
x0 is V11() real ext-real Element of REAL
f is non zero Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(NAT,REAL))
lim f is V11() real ext-real Element of REAL
u is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
lim u is V11() Element of COMPLEX
v is V11() real ext-real Element of REAL
x0 is V11() real ext-real set
z0 is V11() set
y0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V126() V127() V166() V167() V168() V169() V170() V171() Element of NAT
xy0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V126() V127() V166() V167() V168() V169() V170() V171() Element of NAT
gu is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V126() V127() V166() V167() V168() V169() V170() V171() Element of NAT
f . gu is V11() real ext-real Element of REAL
(f . gu) - v is V11() real ext-real Element of REAL
K38(v) is V11() real ext-real set
K36((f . gu),K38(v)) is V11() real ext-real set
|.((f . gu) - v).| is V11() real ext-real Element of REAL
Re ((f . gu) - v) is V11() real ext-real Element of REAL
(Re ((f . gu) - v)) ^2 is V11() real ext-real Element of REAL
Im ((f . gu) - v) is V11() real ext-real Element of REAL
(Im ((f . gu) - v)) ^2 is V11() real ext-real Element of REAL
((Re ((f . gu) - v)) ^2) + ((Im ((f . gu) - v)) ^2) is V11() real ext-real Element of REAL
sqrt (((Re ((f . gu) - v)) ^2) + ((Im ((f . gu) - v)) ^2)) is V11() real ext-real Element of REAL
f is non zero Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(NAT,REAL))
u is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
lim f is V11() real ext-real Element of REAL
lim u is V11() Element of COMPLEX
lim u is V11() Element of COMPLEX
lim f is V11() real ext-real Element of REAL
f is Relation-like COMPLEX -defined COMPLEX -valued Function-like complex-yielding Element of K6(K7(COMPLEX,COMPLEX))
Re f is Relation-like COMPLEX -defined REAL -valued Function-like complex-yielding V115() V116() Element of K6(K7(COMPLEX,REAL))
K7(COMPLEX,REAL) is complex-yielding V115() V116() set
K6(K7(COMPLEX,REAL)) is set
dom (Re f) is V166() Element of K6(COMPLEX)
Im f is Relation-like COMPLEX -defined REAL -valued Function-like complex-yielding V115() V116() Element of K6(K7(COMPLEX,REAL))
dom (Im f) is V166() Element of K6(COMPLEX)
dom f is V166() Element of K6(COMPLEX)
u is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
f is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
<i> (#) f is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
v is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V126() V127() V166() V167() V168() V169() V170() V171() Element of NAT
(<i> (#) f) . v is V11() Element of COMPLEX
f . v is V11() Element of COMPLEX
<i> * (f . v) is V11() Element of COMPLEX
u is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
f is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
<i> (#) f is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
lim f is V11() Element of COMPLEX
lim (<i> (#) f) is V11() Element of COMPLEX
<i> * 0 is V11() Element of COMPLEX
- <i> is V11() Element of COMPLEX
(- <i>) (#) (<i> (#) f) is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
(- <i>) * <i> is V11() Element of COMPLEX
((- <i>) * <i>) (#) f is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
lim (<i> (#) f) is V11() Element of COMPLEX
lim f is V11() Element of COMPLEX
<i> * (lim f) is V11() Element of COMPLEX
REAL 2 is non zero FinSequence-membered M14( REAL )
K434(2,REAL) is FinSequence-membered M14( REAL )
K7((REAL 2),REAL) is complex-yielding V115() V116() set
K6(K7((REAL 2),REAL)) is set
f is Relation-like COMPLEX -defined COMPLEX -valued Function-like complex-yielding Element of K6(K7(COMPLEX,COMPLEX))
dom f is V166() Element of K6(COMPLEX)
Re f is Relation-like COMPLEX -defined REAL -valued Function-like complex-yielding V115() V116() Element of K6(K7(COMPLEX,REAL))
K7(COMPLEX,REAL) is complex-yielding V115() V116() set
K6(K7(COMPLEX,REAL)) is set
Im f is Relation-like COMPLEX -defined REAL -valued Function-like complex-yielding V115() V116() Element of K6(K7(COMPLEX,REAL))
u is Relation-like REAL 2 -defined REAL -valued Function-like complex-yielding V115() V116() Element of K6(K7((REAL 2),REAL))
dom u is Element of K6((REAL 2))
K6((REAL 2)) is set
v is Relation-like REAL 2 -defined REAL -valued Function-like complex-yielding V115() V116() Element of K6(K7((REAL 2),REAL))
dom v is Element of K6((REAL 2))
z0 is V11() set
diff (f,z0) is V11() Element of COMPLEX
Re (diff (f,z0)) is V11() real ext-real Element of REAL
Im (diff (f,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
y0 * <i> is V11() Element of COMPLEX
x0 + (y0 * <i>) is V11() Element of COMPLEX
<*x0,y0*> is set
xy0 is Relation-like NAT -defined REAL -valued Function-like V40(2) FinSequence-like complex-yielding V115() V116() Element of REAL 2
partdiff (u,xy0,1) is V11() real ext-real Element of REAL
reproj (1,xy0) is non zero Relation-like REAL -defined REAL 2 -valued 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
u * (reproj (1,xy0)) is Relation-like REAL -defined REAL -valued Function-like complex-yielding V115() V116() Element of K6(K7(REAL,REAL))
proj (1,2) is non zero Relation-like REAL 2 -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7((REAL 2),REAL))
(proj (1,2)) . xy0 is V11() real ext-real Element of REAL
diff ((u * (reproj (1,xy0))),((proj (1,2)) . xy0)) is V11() real ext-real Element of REAL
partdiff (v,xy0,2) is V11() real ext-real Element of REAL
reproj (2,xy0) is non zero Relation-like REAL -defined REAL 2 -valued Function-like total quasi_total Element of K6(K7(REAL,(REAL 2)))
v * (reproj (2,xy0)) is Relation-like REAL -defined REAL -valued Function-like complex-yielding V115() V116() Element of K6(K7(REAL,REAL))
proj (2,2) is non zero Relation-like REAL 2 -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7((REAL 2),REAL))
(proj (2,2)) . xy0 is V11() real ext-real Element of REAL
diff ((v * (reproj (2,xy0))),((proj (2,2)) . xy0)) is V11() real ext-real Element of REAL
partdiff (u,xy0,2) is V11() real ext-real Element of REAL
u * (reproj (2,xy0)) is Relation-like REAL -defined REAL -valued Function-like complex-yielding V115() V116() Element of K6(K7(REAL,REAL))
diff ((u * (reproj (2,xy0))),((proj (2,2)) . xy0)) is V11() real ext-real Element of REAL
- (partdiff (u,xy0,2)) is V11() real ext-real Element of REAL
partdiff (v,xy0,1) is V11() real ext-real Element of REAL
v * (reproj (1,xy0)) is Relation-like REAL -defined REAL -valued Function-like complex-yielding V115() V116() Element of K6(K7(REAL,REAL))
diff ((v * (reproj (1,xy0))),((proj (1,2)) . xy0)) is V11() real ext-real Element of REAL
gu is non zero Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(REAL,REAL))
Nu is non zero Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(REAL,REAL))
r1 is V11() real ext-real Element of REAL
(v * (reproj (2,xy0))) . r1 is V11() real ext-real Element of REAL
<*x0,r1*> is set
v . <*x0,r1*> is V11() real ext-real Element of REAL
dom (reproj (2,xy0)) is V166() V167() V168() Element of K6(REAL)
(reproj (2,xy0)) . r1 is V40(2) Element of REAL 2
v . ((reproj (2,xy0)) . r1) is V11() real ext-real Element of REAL
Replace (xy0,2,r1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-yielding V115() V116() FinSequence of REAL
v . (Replace (xy0,2,r1)) is V11() real ext-real Element of REAL
r1 is V11() real ext-real Element of REAL
(u * (reproj (2,xy0))) . r1 is V11() real ext-real Element of REAL
<*x0,r1*> is set
u . <*x0,r1*> is V11() real ext-real Element of REAL
dom (reproj (2,xy0)) is V166() V167() V168() Element of K6(REAL)
(reproj (2,xy0)) . r1 is V40(2) Element of REAL 2
u . ((reproj (2,xy0)) . r1) is V11() real ext-real Element of REAL
Replace (xy0,2,r1) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-yielding V115() V116() FinSequence of REAL
u . (Replace (xy0,2,r1)) is V11() real ext-real Element of REAL
xy0 . 2 is V11() real ext-real Element of REAL
gv is non zero Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(REAL,REAL))
- (Im (diff (f,z0))) is V11() real ext-real Element of REAL
gvxy0 is V11() real ext-real Element of REAL
gv . gvxy0 is V11() real ext-real Element of REAL
(- (Im (diff (f,z0)))) * gvxy0 is V11() real ext-real Element of REAL
(Im (diff (f,z0))) * gvxy0 is V11() real ext-real Element of REAL
- ((Im (diff (f,z0))) * gvxy0) is V11() real ext-real Element of REAL
Ru is V11() Element of COMPLEX
diff (f,Ru) is V11() Element of COMPLEX
f /. Ru is V11() Element of COMPLEX
Nv is V166() Neighbourhood of Ru
r2 is non zero Relation-like COMPLEX -defined COMPLEX -valued Function-like total quasi_total complex-yielding linear Element of K6(K7(COMPLEX,COMPLEX))
r2 /. 1r is V11() Element of COMPLEX
r2 . 1r is V11() Element of COMPLEX
r0 is non zero Relation-like COMPLEX -defined COMPLEX -valued Function-like total quasi_total complex-yielding RestFunc-like Element of K6(K7(COMPLEX,COMPLEX))
r2 is non zero Relation-like COMPLEX -defined COMPLEX -valued Function-like total quasi_total complex-yielding linear Element of K6(K7(COMPLEX,COMPLEX))
r2 /. 1r is V11() Element of COMPLEX
r2 . 1r is V11() Element of COMPLEX
r0 is non zero Relation-like COMPLEX -defined COMPLEX -valued Function-like total quasi_total complex-yielding RestFunc-like Element of K6(K7(COMPLEX,COMPLEX))
Im r0 is Relation-like COMPLEX -defined REAL -valued Function-like complex-yielding V115() V116() Element of K6(K7(COMPLEX,REAL))
N is non zero Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(REAL,REAL))
Rv is V11() set
f /. Rv is V11() Element of COMPLEX
(f /. Rv) - (f /. Ru) is V11() Element of COMPLEX
K38((f /. Ru)) is V11() set
K36((f /. Rv),K38((f /. Ru))) is V11() set
Rv - Ru is V11() Element of COMPLEX
K38(Ru) is V11() set
K36(Rv,K38(Ru)) is V11() set
(diff (f,Ru)) * (Rv - Ru) is V11() Element of COMPLEX
r0 /. (Rv - Ru) is V11() Element of COMPLEX
r0 . (Rv - Ru) is V11() Element of COMPLEX
((diff (f,Ru)) * (Rv - Ru)) + (r0 /. (Rv - Ru)) is V11() Element of COMPLEX
a is V11() Element of COMPLEX
N is V11() Element of COMPLEX
N - Ru is V11() Element of COMPLEX
K36(N,K38(Ru)) is V11() set
1r * (N - Ru) is V11() Element of COMPLEX
r2 /. (1r * (N - Ru)) is V11() Element of COMPLEX
r2 . (1r * (N - Ru)) is V11() Element of COMPLEX
a * 1r is V11() Element of COMPLEX
(a * 1r) * (N - Ru) is V11() Element of COMPLEX
(r2 /. 1r) * (N - Ru) is V11() Element of COMPLEX
f . (x0 + (y0 * <i>)) is V11() set
Rv is V11() real ext-real Element of REAL
N is V11() real ext-real Element of REAL
N * <i> is V11() Element of COMPLEX
Rv + (N * <i>) is V11() Element of COMPLEX
f . (Rv + (N * <i>)) is V11() set
(f . (Rv + (N * <i>))) - (f . (x0 + (y0 * <i>))) is V11() Element of COMPLEX
K38((f . (x0 + (y0 * <i>)))) is V11() set
K36((f . (Rv + (N * <i>))),K38((f . (x0 + (y0 * <i>))))) is V11() set
(Rv + (N * <i>)) - (x0 + (y0 * <i>)) is V11() Element of COMPLEX
K38((x0 + (y0 * <i>))) is V11() set
K36((Rv + (N * <i>)),K38((x0 + (y0 * <i>)))) is V11() set
(diff (f,Ru)) * ((Rv + (N * <i>)) - (x0 + (y0 * <i>))) is V11() Element of COMPLEX
r0 /. ((Rv + (N * <i>)) - (x0 + (y0 * <i>))) is V11() Element of COMPLEX
r0 . ((Rv + (N * <i>)) - (x0 + (y0 * <i>))) is V11() Element of COMPLEX
((diff (f,Ru)) * ((Rv + (N * <i>)) - (x0 + (y0 * <i>)))) + (r0 /. ((Rv + (N * <i>)) - (x0 + (y0 * <i>)))) is V11() Element of COMPLEX
f /. (Rv + (N * <i>)) is V11() Element of COMPLEX
f /. (x0 + (y0 * <i>)) is V11() Element of COMPLEX
dom r0 is V166() Element of K6(COMPLEX)
Rv is non zero Relation-like non-empty NAT -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() 0 -convergent convergent Element of K6(K7(NAT,REAL))
Rv " is non zero Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(NAT,REAL))
N /* Rv is non zero Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(NAT,REAL))
(Rv ") (#) (N /* Rv) is non zero Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(NAT,REAL))
lim ((Rv ") (#) (N /* Rv)) is V11() real ext-real Element of REAL
rng Rv is V166() V167() V168() Element of K6(REAL)
N is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
a is non zero Relation-like non-empty NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding 0 -convergent V219() convergent Element of K6(K7(NAT,COMPLEX))
<i> (#) a is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding V219() convergent Element of K6(K7(NAT,COMPLEX))
L is non zero Relation-like non-empty NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding 0 -convergent V219() convergent Element of K6(K7(NAT,COMPLEX))
rng L is V166() Element of K6(COMPLEX)
dom N is V166() V167() V168() Element of K6(REAL)
R is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V126() V127() V166() V167() V168() V169() V170() V171() Element of NAT
Rv . R is V11() real ext-real Element of REAL
(Rv . R) " is V11() real ext-real Element of REAL
Im ((Rv . R) ") is V11() real ext-real Element of REAL
Re ((Rv . R) ") is V11() real ext-real Element of REAL
L . R is V11() Element of COMPLEX
(Rv . R) * <i> is V11() Element of COMPLEX
dom (Im r0) is V166() Element of K6(COMPLEX)
((Rv ") (#) (N /* Rv)) . R is V11() real ext-real Element of REAL
(Rv ") . R is V11() real ext-real Element of REAL
(N /* Rv) . R is V11() real ext-real Element of REAL
((Rv ") . R) * ((N /* Rv) . R) is V11() real ext-real Element of REAL
((Rv . R) ") * ((N /* Rv) . R) is V11() real ext-real Element of REAL
N . (Rv . R) is V11() real ext-real Element of REAL
((Rv . R) ") * (N . (Rv . R)) is V11() real ext-real Element of REAL
(Im r0) . ((Rv . R) * <i>) is V11() real ext-real Element of REAL
((Rv . R) ") * ((Im r0) . ((Rv . R) * <i>)) is V11() real ext-real Element of REAL
r0 . ((Rv . R) * <i>) is V11() Element of COMPLEX
Im (r0 . ((Rv . R) * <i>)) is V11() real ext-real Element of REAL
(Re ((Rv . R) ")) * (Im (r0 . ((Rv . R) * <i>))) is V11() real ext-real Element of REAL
Re (r0 . ((Rv . R) * <i>)) is V11() real ext-real Element of REAL
(Re (r0 . ((Rv . R) * <i>))) * (Im ((Rv . R) ")) is V11() real ext-real Element of REAL
((Re ((Rv . R) ")) * (Im (r0 . ((Rv . R) * <i>)))) + ((Re (r0 . ((Rv . R) * <i>))) * (Im ((Rv . R) "))) is V11() real ext-real Element of REAL
(L . R) / <i> is V11() Element of COMPLEX
K39(<i>) is V11() set
(Re <i>) / (((Re <i>) ^2) + ((Im <i>) ^2)) is V11() real ext-real Element of REAL
- (Im <i>) is V11() real ext-real Element of REAL
(- (Im <i>)) / (((Re <i>) ^2) + ((Im <i>) ^2)) is V11() real ext-real Element of REAL
K37(((- (Im <i>)) / (((Re <i>) ^2) + ((Im <i>) ^2))),<i>) is V11() set
K36(((Re <i>) / (((Re <i>) ^2) + ((Im <i>) ^2))),K37(((- (Im <i>)) / (((Re <i>) ^2) + ((Im <i>) ^2))),<i>)) is V11() set
K37((L . R),K39(<i>)) is V11() set
((L . R) / <i>) " is V11() Element of COMPLEX
Re ((L . R) / <i>) is V11() real ext-real Element of REAL
(Re ((L . R) / <i>)) ^2 is V11() real ext-real Element of REAL
Im ((L . R) / <i>) is V11() real ext-real Element of REAL
(Im ((L . R) / <i>)) ^2 is V11() real ext-real Element of REAL
((Re ((L . R) / <i>)) ^2) + ((Im ((L . R) / <i>)) ^2) is V11() real ext-real Element of REAL
(Re ((L . R) / <i>)) / (((Re ((L . R) / <i>)) ^2) + ((Im ((L . R) / <i>)) ^2)) is V11() real ext-real Element of REAL
K39((((Re ((L . R) / <i>)) ^2) + ((Im ((L . R) / <i>)) ^2))) is V11() real ext-real set
K37((Re ((L . R) / <i>)),K39((((Re ((L . R) / <i>)) ^2) + ((Im ((L . R) / <i>)) ^2)))) is V11() real ext-real set
- (Im ((L . R) / <i>)) is V11() real ext-real Element of REAL
(- (Im ((L . R) / <i>))) / (((Re ((L . R) / <i>)) ^2) + ((Im ((L . R) / <i>)) ^2)) is V11() real ext-real Element of REAL
K37((- (Im ((L . R) / <i>))),K39((((Re ((L . R) / <i>)) ^2) + ((Im ((L . R) / <i>)) ^2)))) is V11() real ext-real set
K37(((- (Im ((L . R) / <i>))) / (((Re ((L . R) / <i>)) ^2) + ((Im ((L . R) / <i>)) ^2))),<i>) is V11() set
K36(((Re ((L . R) / <i>)) / (((Re ((L . R) / <i>)) ^2) + ((Im ((L . R) / <i>)) ^2))),K37(((- (Im ((L . R) / <i>))) / (((Re ((L . R) / <i>)) ^2) + ((Im ((L . R) / <i>)) ^2))),<i>)) is V11() set
r0 . (L . R) is V11() Element of COMPLEX
(((L . R) / <i>) ") * (r0 . (L . R)) is V11() Element of COMPLEX
Im ((((L . R) / <i>) ") * (r0 . (L . R))) is V11() real ext-real Element of REAL
<i> / (L . R) is V11() Element of COMPLEX
K39((L . R)) is V11() set
Re (L . R) is V11() real ext-real Element of REAL
(Re (L . R)) ^2 is V11() real ext-real Element of REAL
Im (L . R) is V11() real ext-real Element of REAL
(Im (L . R)) ^2 is V11() real ext-real Element of REAL
((Re (L . R)) ^2) + ((Im (L . R)) ^2) is V11() real ext-real Element of REAL
(Re (L . R)) / (((Re (L . R)) ^2) + ((Im (L . R)) ^2)) is V11() real ext-real Element of REAL
- (Im (L . R)) is V11() real ext-real Element of REAL
(- (Im (L . R))) / (((Re (L . R)) ^2) + ((Im (L . R)) ^2)) is V11() real ext-real Element of REAL
K37(((- (Im (L . R))) / (((Re (L . R)) ^2) + ((Im (L . R)) ^2))),<i>) is V11() set
K36(((Re (L . R)) / (((Re (L . R)) ^2) + ((Im (L . R)) ^2))),K37(((- (Im (L . R))) / (((Re (L . R)) ^2) + ((Im (L . R)) ^2))),<i>)) is V11() set
K37(<i>,K39((L . R))) is V11() set
(<i> / (L . R)) * (r0 . (L . R)) is V11() Element of COMPLEX
Im ((<i> / (L . R)) * (r0 . (L . R))) is V11() real ext-real Element of REAL
L " is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
(L ") . R is V11() Element of COMPLEX
<i> * ((L ") . R) is V11() Element of COMPLEX
(<i> * ((L ") . R)) * (r0 . (L . R)) is V11() Element of COMPLEX
Im ((<i> * ((L ") . R)) * (r0 . (L . R))) is V11() real ext-real Element of REAL
((L ") . R) * (r0 . (L . R)) is V11() Element of COMPLEX
<i> * (((L ") . R) * (r0 . (L . R))) is V11() Element of COMPLEX
Im (<i> * (((L ") . R) * (r0 . (L . R)))) is V11() real ext-real Element of REAL
r0 /. (L . R) is V11() Element of COMPLEX
((L ") . R) * (r0 /. (L . R)) is V11() Element of COMPLEX
Im (((L ") . R) * (r0 /. (L . R))) is V11() real ext-real Element of REAL
(Re <i>) * (Im (((L ") . R) * (r0 /. (L . R)))) is V11() real ext-real Element of REAL
Re (((L ") . R) * (r0 /. (L . R))) is V11() real ext-real Element of REAL
(Re (((L ") . R) * (r0 /. (L . R)))) * (Im <i>) is V11() real ext-real Element of REAL
((Re <i>) * (Im (((L ") . R) * (r0 /. (L . R))))) + ((Re (((L ") . R) * (r0 /. (L . R)))) * (Im <i>)) is V11() real ext-real Element of REAL
r0 /* L is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
(r0 /* L) . R is V11() Element of COMPLEX
((L ") . R) * ((r0 /* L) . R) is V11() Element of COMPLEX
Re (((L ") . R) * ((r0 /* L) . R)) is V11() real ext-real Element of REAL
(L ") (#) (r0 /* L) is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
((L ") (#) (r0 /* L)) . R is V11() Element of COMPLEX
Re (((L ") (#) (r0 /* L)) . R) is V11() real ext-real Element of REAL
Re ((L ") (#) (r0 /* L)) is non zero Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(NAT,REAL))
lim ((L ") (#) (r0 /* L)) is V11() Element of COMPLEX
Re r0 is Relation-like COMPLEX -defined REAL -valued Function-like complex-yielding V115() V116() Element of K6(K7(COMPLEX,REAL))
N is non zero Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(REAL,REAL))
a is non zero Relation-like non-empty NAT -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() 0 -convergent convergent Element of K6(K7(NAT,REAL))
a " is non zero Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(NAT,REAL))
N /* a is non zero Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(NAT,REAL))
(a ") (#) (N /* a) is non zero Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(NAT,REAL))
lim ((a ") (#) (N /* a)) is V11() real ext-real Element of REAL
rng a is V166() V167() V168() Element of K6(REAL)
L is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
L is non zero Relation-like non-empty NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding 0 -convergent V219() convergent Element of K6(K7(NAT,COMPLEX))
<i> (#) L is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding V219() convergent Element of K6(K7(NAT,COMPLEX))
R is non zero Relation-like non-empty NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding 0 -convergent V219() convergent Element of K6(K7(NAT,COMPLEX))
R " is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
r0 /* R is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
(R ") (#) (r0 /* R) is non zero Relation-like NAT -defined COMPLEX -valued Function-like total quasi_total complex-yielding Element of K6(K7(NAT,COMPLEX))
rng R is V166() Element of K6(COMPLEX)
dom N is V166() V167() V168() Element of K6(REAL)
z0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V126() V127() V166() V167() V168() V169() V170() V171() Element of NAT
a . z0 is V11() real ext-real Element of REAL
(a . z0) " is V11() real ext-real Element of REAL
Im ((a . z0) ") is V11() real ext-real Element of REAL
Re ((a . z0) ") is V11() real ext-real Element of REAL
R . z0 is V11() Element of COMPLEX
(a . z0) * <i> is V11() Element of COMPLEX
dom (Re r0) is V166() Element of K6(COMPLEX)
r0 . (R . z0) is V11() Element of COMPLEX
r0 /. (R . z0) is V11() Element of COMPLEX
((a ") (#) (N /* a)) . z0 is V11() real ext-real Element of REAL
(a ") . z0 is V11() real ext-real Element of REAL
(N /* a) . z0 is V11() real ext-real Element of REAL
((a ") . z0) * ((N /* a) . z0) is V11() real ext-real Element of REAL
((a . z0) ") * ((N /* a) . z0) is V11() real ext-real Element of REAL
N . (a . z0) is V11() real ext-real Element of REAL
((a . z0) ") * (N . (a . z0)) is V11() real ext-real Element of REAL
(Re r0) . ((a . z0) * <i>) is V11() real ext-real Element of REAL
((a . z0) ") * ((Re r0) . ((a . z0) * <i>)) is V11() real ext-real Element of REAL
r0 . ((a . z0) * <i>) is V11() Element of COMPLEX
Re (r0 . ((a . z0) * <i>)) is V11() real ext-real Element of REAL
(Re ((a . z0) ")) * (Re (r0 . ((a . z0) * <i>))) is V11() real ext-real Element of REAL
Im (r0 . ((a . z0) * <i>)) is V11() real ext-real Element of REAL
(Im ((a . z0) ")) * (Im (r0 . ((a . z0) * <i>))) is V11() real ext-real Element of REAL
((Re ((a . z0) ")) * (Re (r0 . ((a . z0) * <i>)))) - ((Im ((a . z0) ")) * (Im (r0 . ((a . z0) * <i>)))) is V11() real ext-real Element of REAL
K38(((Im ((a . z0) ")) * (Im (r0 . ((a . z0) * <i>))))) is V11() real ext-real set
K36(((Re ((a . z0) ")) * (Re (r0 . ((a . z0) * <i>)))),K38(((Im ((a . z0) ")) * (Im (r0 . ((a . z0) * <i>)))))) is V11() real ext-real set
(R . z0) / <i> is V11() Element of COMPLEX
K39(<i>) is V11() set
(Re <i>) / (((Re <i>) ^2) + ((Im <i>) ^2)) is V11() real ext-real Element of REAL
- (Im <i>) is V11() real ext-real Element of REAL
(- (Im <i>)) / (((Re <i>) ^2) + ((Im <i>) ^2)) is V11() real ext-real Element of REAL
K37(((- (Im <i>)) / (((Re <i>) ^2) + ((Im <i>) ^2))),<i>) is V11() set
K36(((Re <i>) / (((Re <i>) ^2) + ((Im <i>) ^2))),K37(((- (Im <i>)) / (((Re <i>) ^2) + ((Im <i>) ^2))),<i>)) is V11() set
K37((R . z0),K39(<i>)) is V11() set
((R . z0) / <i>) " is V11() Element of COMPLEX
Re ((R . z0) / <i>) is V11() real ext-real Element of REAL
(Re ((R . z0) / <i>)) ^2 is V11() real ext-real Element of REAL
Im ((R . z0) / <i>) is V11() real ext-real Element of REAL
(Im ((R . z0) / <i>)) ^2 is V11() real ext-real Element of REAL
((Re ((R . z0) / <i>)) ^2) + ((Im ((R . z0) / <i>)) ^2) is V11() real ext-real Element of REAL
(Re ((R . z0) / <i>)) / (((Re ((R . z0) / <i>)) ^2) + ((Im ((R . z0) / <i>)) ^2)) is V11() real ext-real Element of REAL
K39((((Re ((R . z0) / <i>)) ^2) + ((Im ((R . z0) / <i>)) ^2))) is V11() real ext-real set
K37((Re ((R . z0) / <i>)),K39((((Re ((R . z0) / <i>)) ^2) + ((Im ((R . z0) / <i>)) ^2)))) is V11() real ext-real set
- (Im ((R . z0) / <i>)) is V11() real ext-real Element of REAL
(- (Im ((R . z0) / <i>))) / (((Re ((R . z0) / <i>)) ^2) + ((Im ((R . z0) / <i>)) ^2)) is V11() real ext-real Element of REAL
K37((- (Im ((R . z0) / <i>))),K39((((Re ((R . z0) / <i>)) ^2) + ((Im ((R . z0) / <i>)) ^2)))) is V11() real ext-real set
K37(((- (Im ((R . z0) / <i>))) / (((Re ((R . z0) / <i>)) ^2) + ((Im ((R . z0) / <i>)) ^2))),<i>) is V11() set
K36(((Re ((R . z0) / <i>)) / (((Re ((R . z0) / <i>)) ^2) + ((Im ((R . z0) / <i>)) ^2))),K37(((- (Im ((R . z0) / <i>))) / (((Re ((R . z0) / <i>)) ^2) + ((Im ((R . z0) / <i>)) ^2))),<i>)) is V11() set
(((R . z0) / <i>) ") * (r0 . (R . z0)) is V11() Element of COMPLEX
Re ((((R . z0) / <i>) ") * (r0 . (R . z0))) is V11() real ext-real Element of REAL
<i> / (R . z0) is V11() Element of COMPLEX
K39((R . z0)) is V11() set
Re (R . z0) is V11() real ext-real Element of REAL
(Re (R . z0)) ^2 is V11() real ext-real Element of REAL
Im (R . z0) is V11() real ext-real Element of REAL
(Im (R . z0)) ^2 is V11() real ext-real Element of REAL
((Re (R . z0)) ^2) + ((Im (R . z0)) ^2) is V11() real ext-real Element of REAL
(Re (R . z0)) / (((Re (R . z0)) ^2) + ((Im (R . z0)) ^2)) is V11() real ext-real Element of REAL
- (Im (R . z0)) is V11() real ext-real Element of REAL
(- (Im (R . z0))) / (((Re (R . z0)) ^2) + ((Im (R . z0)) ^2)) is V11() real ext-real Element of REAL
K37(((- (Im (R . z0))) / (((Re (R . z0)) ^2) + ((Im (R . z0)) ^2))),<i>) is V11() set
K36(((Re (R . z0)) / (((Re (R . z0)) ^2) + ((Im (R . z0)) ^2))),K37(((- (Im (R . z0))) / (((Re (R . z0)) ^2) + ((Im (R . z0)) ^2))),<i>)) is V11() set
K37(<i>,K39((R . z0))) is V11() set
(<i> / (R . z0)) * (r0 . (R . z0)) is V11() Element of COMPLEX
Re ((<i> / (R . z0)) * (r0 . (R . z0))) is V11() real ext-real Element of REAL
(R ") . z0 is V11() Element of COMPLEX
<i> * ((R ") . z0) is V11() Element of COMPLEX
(<i> * ((R ") . z0)) * (r0 . (R . z0)) is V11() Element of COMPLEX
Re ((<i> * ((R ") . z0)) * (r0 . (R . z0))) is V11() real ext-real Element of REAL
((R ") . z0) * (r0 . (R . z0)) is V11() Element of COMPLEX
<i> * (((R ") . z0) * (r0 . (R . z0))) is V11() Element of COMPLEX
Re (<i> * (((R ") . z0) * (r0 . (R . z0)))) is V11() real ext-real Element of REAL
Re (((R ") . z0) * (r0 . (R . z0))) is V11() real ext-real Element of REAL
(Re <i>) * (Re (((R ") . z0) * (r0 . (R . z0)))) is V11() real ext-real Element of REAL
Im (((R ") . z0) * (r0 . (R . z0))) is V11() real ext-real Element of REAL
(Im <i>) * (Im (((R ") . z0) * (r0 . (R . z0)))) is V11() real ext-real Element of REAL
((Re <i>) * (Re (((R ") . z0) * (r0 . (R . z0))))) - ((Im <i>) * (Im (((R ") . z0) * (r0 . (R . z0))))) is V11() real ext-real Element of REAL
K38(((Im <i>) * (Im (((R ") . z0) * (r0 . (R . z0)))))) is V11() real ext-real set
K36(((Re <i>) * (Re (((R ") . z0) * (r0 . (R . z0))))),K38(((Im <i>) * (Im (((R ") . z0) * (r0 . (R . z0))))))) is V11() real ext-real set
(r0 /* R) . z0 is V11() Element of COMPLEX
((R ") . z0) * ((r0 /* R) . z0) is V11() Element of COMPLEX
Im (((R ") . z0) * ((r0 /* R) . z0)) is V11() real ext-real Element of REAL
- (Im (((R ") . z0) * ((r0 /* R) . z0))) is V11() real ext-real Element of REAL
((R ") (#) (r0 /* R)) . z0 is V11() Element of COMPLEX
Im (((R ") (#) (r0 /* R)) . z0) is V11() real ext-real Element of REAL
- (Im (((R ") (#) (r0 /* R)) . z0)) is V11() real ext-real Element of REAL
Im ((R ") (#) (r0 /* R)) is non zero Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(NAT,REAL))
(Im ((R ") (#) (r0 /* R))) . z0 is V11() real ext-real Element of REAL
- ((Im ((R ") (#) (r0 /* R))) . z0) is V11() real ext-real Element of REAL
- (Im ((R ") (#) (r0 /* R))) is non zero Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V115() V116() Element of K6(K7(NAT,REAL))
K38(1) is non zero V11() real ext-real non positive negative set
K38(1) (#) (Im ((R ") (#) (r0 /* R))) is Relation-like NAT -defined Function-like total complex-yielding V115() V116() set
lim ((R ") (#) (r0 /* R)) is V11() Element of COMPLEX
lim (Im ((R ") (#) (r0 /* R))) is V11() real ext-real Element of REAL
- (Im 0) is V11() real ext-real Element of REAL
L is V11() real ext-real Element of REAL
{ b1 where b1 is V11() set : not L <= |.(b1 - Ru).| } is set
y0 - L is V11() real ext-real Element of REAL
K38(L) is V11() real ext-real set
K36(y0,K38(L)) is V11() real ext-real set
y0 + L is V11() real ext-real Element of REAL
].(y0 - L),(y0 + L).[ is V166() V167() V168() Element of K6(REAL)
R is V166() V167() V168() Neighbourhood of y0
R is V11() real ext-real Element of REAL
R * <i> is V11() Element of COMPLEX
x0 + (R * <i>) is V11() Element of COMPLEX
(x0 + (R * <i>)) - Ru is V11() Element of COMPLEX
K38(Ru) is V11() set
K36((x0 + (R * <i>)),K38(Ru)) is V11() set
|.((x0 + (R * <i>)) - Ru).| is V11() real ext-real Element of REAL
Re ((x0 + (R * <i>)) - Ru) is V11() real ext-real Element of REAL
(Re ((x0 + (R * <i>)) - Ru)) ^2 is V11() real ext-real Element of REAL
Im ((x0 + (R * <i>)) - Ru) is V11() real ext-real Element of REAL
(Im ((x0 + (R * <i>)) - Ru)) ^2 is V11() real ext-real Element of REAL
((Re ((x0 + (R * <i>)) - Ru)) ^2) + ((Im ((x0 + (R * <i>)) - Ru)) ^2) is V11() real ext-real Element of REAL
sqrt (((Re ((x0 + (R * <i>)) - Ru)) ^2) + ((Im ((x0 + (R * <i>)) - Ru)) ^2)) is V11() real ext-real Element of REAL
R - y0 is V11() real ext-real Element of REAL
K38(y0) is V11() real ext-real set
K36(R,K38(y0)) is V11() real ext-real set
(R - y0) * <i> is V11() Element of COMPLEX
|.((R - y0) * <i>).| is V11() real ext-real Element of REAL
Re ((R - y0) * <i>) is V11() real ext-real Element of REAL
(Re ((R - y0) * <i>)) ^2 is V11() real ext-real Element of REAL
Im ((R - y0) * <i>) is V11() real ext-real Element of REAL
(Im ((R - y0) * <i>)) ^2 is V11() real ext-real Element of REAL
((Re ((R - y0) * <i>)) ^2) + ((Im ((R - y0) * <i>)) ^2) is V11() real ext-real Element of REAL
sqrt (((Re ((R - y0) * <i>)) ^2) + ((Im ((R - y0) * <i>)) ^2)) is V11() real ext-real Element of REAL
|.(R - y0).| is V11() real ext-real Element of REAL
Re (R - y0) is V11() real ext-real Element of REAL
(Re (R - y0)) ^2 is V11() real ext-real Element of REAL
Im (R - y0) is V11() real ext-real Element of REAL
(Im (R - y0)) ^2 is V11() real ext-real Element of REAL
((Re (R - y0)) ^2) + ((Im (R - y0)) ^2) is V11() real ext-real Element of REAL
sqrt (((Re (R - y0)) ^2) + ((Im (R - y0)) ^2)) is V11() real ext-real Element of REAL
|.(R - y0).| * |.<i>.| is V11() real ext-real Element of REAL
Re (diff (f,Ru)) is V11() real ext-real Element of REAL
Im (diff (f,Ru)) is V11() real ext-real Element of REAL
R is V11() real ext-real Element of REAL
z0 is V11() real ext-real Element of REAL
z0 * <i> is V11() Element of COMPLEX
R + (z0 * <i>) is V11() Element of COMPLEX
(R + (z0 * <i>)) - (x0 + (y0 * <i>)) is V11() Element of COMPLEX
K38((x0 + (y0 * <i>))) is V11() set
K36((R + (z0 * <i>)),K38((x0 + (y0 * <i>)))) is V11() set
(diff (f,Ru)) * ((R + (z0 * <i>)) - (x0 + (y0 * <i>))) is V11() Element of COMPLEX
R - x0 is V11() real ext-real Element of REAL
K38(x0) is V11() real ext-real set
K36(R,K38(x0)) is V11() real ext-real set
(Re (diff (f,Ru))) * (R - x0) is V11() real ext-real Element of REAL
z0 - y0 is V11() real ext-real Element of REAL
K38(y0) is V11() real ext-real set
K36(z0,K38(y0)) is V11() real ext-real set
(Im (diff (f,Ru))) * (z0 - y0) is V11() real ext-real Element of REAL
((Re (diff (f,Ru))) * (R - x0)) - ((Im (diff (f,Ru))) * (z0 - y0)) is V11() real ext-real Element of REAL
K38(((Im (diff (f,Ru))) * (z0 - y0))) is V11() real ext-real set
K36(((Re (diff (f,Ru))) * (R - x0)),K38(((Im (diff (f,Ru))) * (z0 - y0)))) is V11() real ext-real set
(Im (diff (f,Ru))) * (R - x0) is V11() real ext-real Element of REAL
(Re (diff (f,Ru))) * (z0 - y0) is V11() real ext-real Element of REAL
((Im (diff (f,Ru))) * (R - x0)) + ((Re (diff (f,Ru))) * (z0 - y0)) is V11() real ext-real Element of REAL
(((Im (diff (f,Ru))) * (R - x0)) + ((Re (diff (f,Ru))) * (z0 - y0))) * <i> is V11() Element of COMPLEX
(((Re (diff (f,Ru))) * (R - x0)) - ((Im (diff (f,Ru))) * (z0 - y0))) + ((((Im (diff (f,Ru))) * (R - x0)) + ((Re (diff (f,Ru))) * (z0 - y0))) * <i>) is V11() Element of COMPLEX
(Im (diff (f,Ru))) * <i> is V11() Element of COMPLEX
(Re (diff (f,Ru))) + ((Im (diff (f,Ru))) * <i>) is V11() Element of COMPLEX
(z0 - y0) * <i> is V11() Element of COMPLEX
(R - x0) + ((z0 - y0) * <i>) is V11() Element of COMPLEX
((Re (diff (f,Ru))) + ((Im (diff (f,Ru))) * <i>)) * ((R - x0) + ((z0 - y0) * <i>)) is V11() Element of COMPLEX
R is V11() real ext-real Element of REAL
z0 is V11() real ext-real Element of REAL
z0 * <i> is V11() Element of COMPLEX
R + (z0 * <i>) is V11() Element of COMPLEX
(R + (z0 * <i>)) - (x0 + (y0 * <i>)) is V11() Element of COMPLEX
K38((x0 + (y0 * <i>))) is V11() set
K36((R + (z0 * <i>)),K38((x0 + (y0 * <i>)))) is V11() set
(diff (f,Ru)) * ((R + (z0 * <i>)) - (x0 + (y0 * <i>))) is V11() Element of COMPLEX
Re ((diff (f,Ru)) * ((R + (z0 * <i>)) - (x0 + (y0 * <i>)))) is V11() real ext-real Element of REAL
R - x0 is V11() real ext-real Element of REAL
K38(x0) is V11() real ext-real set
K36(R,K38(x0)) is V11() real ext-real set
(Re (diff (f,Ru))) * (R - x0) is V11() real ext-real Element of REAL
z0 - y0 is V11() real ext-real Element of REAL
K38(y0) is V11() real ext-real set
K36(z0,K38(y0)) is V11() real ext-real set
(Im (diff (f,Ru))) * (z0 - y0) is V11() real ext-real Element of REAL
((Re (diff (f,Ru))) * (R - x0)) - ((Im (diff (f,Ru))) * (z0 - y0)) is V11() real ext-real Element of REAL
K38(((Im (diff (f,Ru))) * (z0 - y0))) is V11() real ext-real set
K36(((Re (diff (f,Ru))) * (R - x0)),K38(((Im (diff (f,Ru))) * (z0 - y0)))) is V11() real ext-real set
(Im (diff (f,Ru))) * (R - x0) is V11() real ext-real Element of REAL
(Re (diff (f,Ru))) * (z0 - y0) is V11() real ext-real Element of REAL
((Im (diff (f,Ru))) * (R - x0)) + ((Re (diff (f,Ru))) * (z0 - y0)) is V11() real ext-real Element of REAL
(((Im (diff (f,Ru))) * (R - x0)) + ((Re (diff (f,Ru))) * (z0 - y0))) * <i> is V11() Element of COMPLEX
(((Re (diff (f,Ru))) * (R - x0)) - ((Im (diff (f,Ru))) * (z0 - y0))) + ((((Im (diff (f,Ru))) * (R - x0)) + ((Re (diff (f,Ru))) * (z0 - y0))) * <i>) is V11() Element of COMPLEX
Re ((((Re (diff (f,Ru))) * (R - x0)) - ((Im (diff (f,Ru))) * (z0 - y0))) + ((((Im (diff (f,Ru))) * (R - x0)) + ((Re (diff (f,Ru))) * (z0 - y0))) * <i>)) is V11() real ext-real Element of REAL
u . <*x0,y0*> is V11() real ext-real Element of REAL
x0 - x0 is V11() real ext-real Element of REAL
K38(x0) is V11() real ext-real set
K36(x0,K38(x0)) is V11() real ext-real set
R is V11() real ext-real Element of REAL
<*x0,R*> is set
u . <*x0,R*> is V11() real ext-real Element of REAL
(u . <*x0,R*>) - (u . <*x0,y0*>) is V11() real ext-real Element of REAL
K38((u . <*x0,y0*>)) is V11() real ext-real set
K36((u . <*x0,R*>),K38((u . <*x0,y0*>))) is V11() real ext-real set
R - y0 is V11() real ext-real Element of REAL
K38(y0) is V11() real ext-real set
K36(R,K38(y0)) is V11() real ext-real set
(Im (diff (f,Ru))) * (R - y0) is V11() real ext-real Element of REAL
- ((Im (diff (f,Ru))) * (R - y0)) is V11() real ext-real Element of REAL
(R - y0) * <i> is V11() Element of COMPLEX
(x0 - x0) + ((R - y0) * <i>) is V11() Element of COMPLEX
(Re r0) . ((x0 - x0) + ((R - y0) * <i>)) is V11() real ext-real Element of REAL
(- ((Im (diff (f,Ru))) * (R - y0))) + ((Re r0) . ((x0 - x0) + ((R - y0) * <i>))) is V11() real ext-real Element of REAL
R * <i> is V11() Element of COMPLEX
x0 + (R * <i>) is V11() Element of COMPLEX
(x0 + (R * <i>)) - (x0 + (y0 * <i>)) is V11() Element of COMPLEX
K38((x0 + (y0 * <i>))) is V11() set
K36((x0 + (R * <i>)),K38((x0 + (y0 * <i>)))) is V11() set
dom (Re r0) is V166() Element of K6(COMPLEX)
dom (Re f) is V166() Element of K6(COMPLEX)
(Re f) . (x0 + (R * <i>)) is V11() real ext-real Element of REAL
((Re f) . (x0 + (R * <i>))) - (u . <*x0,y0*>) is V11() real ext-real Element of REAL
K36(((Re f) . (x0 + (R * <i>))),K38((u . <*x0,y0*>))) is V11() real ext-real set
(Re f) . (x0 + (y0 * <i>)) is V11() real ext-real Element of REAL
((Re f) . (x0 + (R * <i>))) - ((Re f) . (x0 + (y0 * <i>))) is V11() real ext-real Element of REAL
K38(((Re f) . (x0 + (y0 * <i>)))) is V11() real ext-real set
K36(((Re f) . (x0 + (R * <i>))),K38(((Re f) . (x0 + (y0 * <i>))))) is V11() real ext-real set
f . (x0 + (R * <i>)) is V11() set
Re (f . (x0 + (R * <i>))) is V11() real ext-real Element of REAL
(Re (f . (x0 + (R * <i>)))) - ((Re f) . (x0 + (y0 * <i>))) is V11() real ext-real Element of REAL
K36((Re (f . (x0 + (R * <i>)))),K38(((Re f) . (x0 + (y0 * <i>))))) is V11() real ext-real set
Re (f . (x0 + (y0 * <i>))) is V11() real ext-real Element of REAL
(Re (f . (x0 + (R * <i>)))) - (Re (