for f being ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -valued Function-like complex-yielding ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -valued Function-like complex-yielding ) PartFunc of ,) is total holds
( dom (Re f : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -valued Function-like complex-yielding ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) Element of K6(K7(COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ,REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( complex-yielding V115() V116() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V166() ) Element of K6(COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) : ( ( ) ( ) set ) ) = COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) & dom (Im f : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -valued Function-like complex-yielding ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) Element of K6(K7(COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ,REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( complex-yielding V115() V116() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V166() ) Element of K6(COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) : ( ( ) ( ) set ) ) = COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) ;

for f being ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -valued Function-like complex-yielding ) PartFunc of ,)
for u, v being ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,)
for z0 being ( ( V11() ) ( V11() ) Complex)
for x0, y0 being ( ( ) ( V11() real ext-real ) Real)
for xy0 being ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) st ( for x, y being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Real) + (y : ( ( ) ( V11() real ext-real ) Real) * <i> : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) in dom f : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -valued Function-like complex-yielding ) PartFunc of ,) : ( ( ) ( V166() ) Element of K6(COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) : ( ( ) ( ) set ) ) holds
( <*x : ( ( ) ( V11() real ext-real ) Real) ,y : ( ( ) ( V11() real ext-real ) Real) *> : ( ( ) ( ) set ) in dom u : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) : ( ( ) ( ) Element of K6((REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) : ( ( ) ( ) set ) ) & u : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) . <*x : ( ( ) ( V11() real ext-real ) Real) ,y : ( ( ) ( V11() real ext-real ) Real) *> : ( ( ) ( ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) = (Re f : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -valued Function-like complex-yielding ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) Element of K6(K7(COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ,REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( complex-yielding V115() V116() ) set ) ) : ( ( ) ( ) set ) ) . (x : ( ( ) ( V11() real ext-real ) Real) + (y : ( ( ) ( V11() real ext-real ) Real) * <i> : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) ) ) & ( for x, y being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Real) + (y : ( ( ) ( V11() real ext-real ) Real) * <i> : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) in dom f : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -valued Function-like complex-yielding ) PartFunc of ,) : ( ( ) ( V166() ) Element of K6(COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) : ( ( ) ( ) set ) ) holds
( <*x : ( ( ) ( V11() real ext-real ) Real) ,y : ( ( ) ( V11() real ext-real ) Real) *> : ( ( ) ( ) set ) in dom v : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) : ( ( ) ( ) Element of K6((REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) : ( ( ) ( ) set ) ) & v : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) . <*x : ( ( ) ( V11() real ext-real ) Real) ,y : ( ( ) ( V11() real ext-real ) Real) *> : ( ( ) ( ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) = (Im f : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -valued Function-like complex-yielding ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) Element of K6(K7(COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ,REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( complex-yielding V115() V116() ) set ) ) : ( ( ) ( ) set ) ) . (x : ( ( ) ( V11() real ext-real ) Real) + (y : ( ( ) ( V11() real ext-real ) Real) * <i> : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) ) ) & z0 : ( ( V11() ) ( V11() ) Complex) = x0 : ( ( ) ( V11() real ext-real ) Real) + (y0 : ( ( ) ( V11() real ext-real ) Real) * <i> : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) & xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) = <*x0 : ( ( ) ( V11() real ext-real ) Real) ,y0 : ( ( ) ( V11() real ext-real ) Real) *> : ( ( ) ( ) set ) & f : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -valued Function-like complex-yielding ) PartFunc of ,) is_differentiable_in z0 : ( ( V11() ) ( V11() ) Complex) holds
( u : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) is_partial_differentiable_in xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) ,1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) & u : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) is_partial_differentiable_in xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) ,2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) & v : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) is_partial_differentiable_in xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) ,1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) & v : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) is_partial_differentiable_in xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) ,2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) & Re (diff (f : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -valued Function-like complex-yielding ) PartFunc of ,) ,z0 : ( ( V11() ) ( V11() ) Complex) )) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) = partdiff (u : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) ,xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) ,1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) & Re (diff (f : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -valued Function-like complex-yielding ) PartFunc of ,) ,z0 : ( ( V11() ) ( V11() ) Complex) )) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) = partdiff (v : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) ,xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) ,2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) & Im (diff (f : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -valued Function-like complex-yielding ) PartFunc of ,) ,z0 : ( ( V11() ) ( V11() ) Complex) )) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) = - (partdiff (u : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) ,xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) ,2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) & Im (diff (f : ( ( Function-like ) ( Relation-like COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -defined COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) -valued Function-like complex-yielding ) PartFunc of ,) ,z0 : ( ( V11() ) ( V11() ) Complex) )) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non zero V33() V166() V172() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) = partdiff (v : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) ,xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) ,1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) ) ;

for seq being ( ( Function-like quasi_total ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like total quasi_total complex-yielding V115() V116() ) Real_Sequence) holds
( seq : ( ( Function-like quasi_total ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like total quasi_total complex-yielding V115() V116() ) Real_Sequence) is convergent & lim seq : ( ( Function-like quasi_total ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like total quasi_total complex-yielding V115() V116() ) Real_Sequence) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) = 0 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) iff ( abs seq : ( ( Function-like quasi_total ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like total quasi_total complex-yielding V115() V116() ) Real_Sequence) : ( ( Function-like ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like total quasi_total complex-yielding V115() V116() ) Element of K6(K7(NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( complex-yielding V115() V116() ) set ) ) : ( ( ) ( ) set ) ) is convergent & lim (abs seq : ( ( Function-like quasi_total ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like total quasi_total complex-yielding V115() V116() ) Real_Sequence) ) : ( ( Function-like ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like total quasi_total complex-yielding V115() V116() ) Element of K6(K7(NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( complex-yielding V115() V116() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) = 0 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ;

for X being ( ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) RealNormSpace)
for seq being ( ( Function-like quasi_total ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b₁ : ( ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non zero ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non zero ) set ) ) holds
( seq : ( ( Function-like quasi_total ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b₁ : ( ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non zero ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non zero ) set ) ) is convergent & lim seq : ( ( Function-like quasi_total ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b₁ : ( ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non zero ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non zero ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non zero ) set ) ) = 0. X : ( ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) RealNormSpace) : ( ( ) ( zero ) Element of the carrier of b₁ : ( ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non zero ) set ) ) iff ( ||.seq : ( ( Function-like quasi_total ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b₁ : ( ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non zero ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non zero ) set ) ) .|| : ( ( Function-like quasi_total ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like total quasi_total complex-yielding V115() V116() ) Element of K6(K7(NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( complex-yielding V115() V116() ) set ) ) : ( ( ) ( ) set ) ) is convergent & lim ||.seq : ( ( Function-like quasi_total ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of b₁ : ( ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) ( V45() V71() V96() V97() V98() V99() V100() V101() V102() V106() V107() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non zero ) set ) -valued Function-like total quasi_total ) sequence of ( ( ) ( non zero ) set ) ) .|| : ( ( Function-like quasi_total ) ( non zero Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like total quasi_total complex-yielding V115() V116() ) Element of K6(K7(NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( complex-yielding V115() V116() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) = 0 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ;

for u being ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,)
for x0, y0 being ( ( ) ( V11() real ext-real ) Real)
for xy0 being ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) st xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) = <*x0 : ( ( ) ( V11() real ext-real ) Real) ,y0 : ( ( ) ( V11() real ext-real ) Real) *> : ( ( ) ( ) set ) & <>* u : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL 1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -valued Function-like ) Element of K6(K7((REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ,(REAL 1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_in xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) holds
( u : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) is_partial_differentiable_in xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) ,1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) & u : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) is_partial_differentiable_in xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) ,2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) & <*(partdiff (u : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) ,xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) ,1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like FinSequence-like complex-yielding V115() V116() ) FinSequence of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) = (diff ((<>* u : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL 1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -valued Function-like ) Element of K6(K7((REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ,(REAL 1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) )) : ( ( Function-like quasi_total ) ( non zero Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL 1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -valued Function-like total quasi_total ) Element of K6(K7((REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ,(REAL 1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . <*1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) *> : ( ( ) ( ) set ) : ( ( ) ( ) set ) & <*(partdiff (u : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) ,xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) ,2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like FinSequence-like complex-yielding V115() V116() ) FinSequence of REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) = (diff ((<>* u : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like complex-yielding V115() V116() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL 1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -valued Function-like ) Element of K6(K7((REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ,(REAL 1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,xy0 : ( ( ) ( Relation-like NAT : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) -valued Function-like V40(2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V115() V116() ) Element of REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) )) : ( ( Function-like quasi_total ) ( non zero Relation-like REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -defined REAL 1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) -valued Function-like total quasi_total ) Element of K6(K7((REAL 2 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ,(REAL 1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero FinSequence-membered ) M14( REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) )) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . <*0 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( 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 : ( ( ) ( non zero epsilon-transitive epsilon-connected ordinal V166() V167() V168() V169() V170() V171() V172() ) Element of K6(REAL : ( ( ) ( non zero V33() V166() V167() V168() V172() ) set ) ) : ( ( ) ( ) set ) ) ) *> : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;