pred f is_hpartial_differentiable`11_in u means :: PDIFF_5:def 1
ex x0, y0, z0 being ( ( ) ( V11() real ext-real ) Real) st
( u : ( ( ) ( ) set ) = <*x0 : ( ( ) ( V11() real ext-real ) Real) ,y0 : ( ( ) ( V11() real ext-real ) Real) ,z0 : ( ( ) ( V11() real ext-real ) Real) *> : ( ( ) ( ) set ) & ex N being ( ( ) ( V160() V161() V162() ) Neighbourhood of x0 : ( ( ) ( V11() real ext-real ) Real) ) st
( N : ( ( ) ( V160() V161() V162() ) Neighbourhood of b₃ : ( ( ) ( V11() real ext-real ) Real) ) c= dom (SVF1 (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V160() V161() V162() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) & ex L being ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) ex R being ( ( V21() RestFunc-like ) ( V1() V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) st
for x being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Real) in N : ( ( ) ( V160() V161() V162() ) Neighbourhood of b₃ : ( ( ) ( V11() real ext-real ) Real) ) holds
((SVF1 (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) - ((SVF1 (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . x0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) = (L : ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) . (x : ( ( ) ( V11() real ext-real ) Real) - x0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) + (R : ( ( V21() RestFunc-like ) ( V1() V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) . (x : ( ( ) ( V11() real ext-real ) Real) - x0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) );

pred f is_hpartial_differentiable`12_in u means :: PDIFF_5:def 2
ex x0, y0, z0 being ( ( ) ( V11() real ext-real ) Real) st
( u : ( ( ) ( ) set ) = <*x0 : ( ( ) ( V11() real ext-real ) Real) ,y0 : ( ( ) ( V11() real ext-real ) Real) ,z0 : ( ( ) ( V11() real ext-real ) Real) *> : ( ( ) ( ) set ) & ex N being ( ( ) ( V160() V161() V162() ) Neighbourhood of y0 : ( ( ) ( V11() real ext-real ) Real) ) st
( N : ( ( ) ( V160() V161() V162() ) Neighbourhood of b₃ : ( ( ) ( V11() real ext-real ) Real) ) c= dom (SVF1 (2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V160() V161() V162() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) & ex L being ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) ex R being ( ( V21() RestFunc-like ) ( V1() V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) st
for y being ( ( ) ( V11() real ext-real ) Real) st y : ( ( ) ( V11() real ext-real ) Real) in N : ( ( ) ( V160() V161() V162() ) Neighbourhood of b₃ : ( ( ) ( V11() real ext-real ) Real) ) holds
((SVF1 (2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) - ((SVF1 (2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . y0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) = (L : ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) . (y : ( ( ) ( V11() real ext-real ) Real) - y0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) + (R : ( ( V21() RestFunc-like ) ( V1() V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) . (y : ( ( ) ( V11() real ext-real ) Real) - y0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) );

pred f is_hpartial_differentiable`13_in u means :: PDIFF_5:def 3
ex x0, y0, z0 being ( ( ) ( V11() real ext-real ) Real) st
( u : ( ( ) ( ) set ) = <*x0 : ( ( ) ( V11() real ext-real ) Real) ,y0 : ( ( ) ( V11() real ext-real ) Real) ,z0 : ( ( ) ( V11() real ext-real ) Real) *> : ( ( ) ( ) set ) & ex N being ( ( ) ( V160() V161() V162() ) Neighbourhood of z0 : ( ( ) ( V11() real ext-real ) Real) ) st
( N : ( ( ) ( V160() V161() V162() ) Neighbourhood of b₃ : ( ( ) ( V11() real ext-real ) Real) ) c= dom (SVF1 (3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V160() V161() V162() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) & ex L being ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) ex R being ( ( V21() RestFunc-like ) ( V1() V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) st
for z being ( ( ) ( V11() real ext-real ) Real) st z : ( ( ) ( V11() real ext-real ) Real) in N : ( ( ) ( V160() V161() V162() ) Neighbourhood of b₃ : ( ( ) ( V11() real ext-real ) Real) ) holds
((SVF1 (3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . z : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) - ((SVF1 (3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . z0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) = (L : ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) . (z : ( ( ) ( V11() real ext-real ) Real) - z0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) + (R : ( ( V21() RestFunc-like ) ( V1() V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) . (z : ( ( ) ( V11() real ext-real ) Real) - z0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) );

pred f is_hpartial_differentiable`21_in u means :: PDIFF_5:def 4
ex x0, y0, z0 being ( ( ) ( V11() real ext-real ) Real) st
( u : ( ( ) ( ) set ) = <*x0 : ( ( ) ( V11() real ext-real ) Real) ,y0 : ( ( ) ( V11() real ext-real ) Real) ,z0 : ( ( ) ( V11() real ext-real ) Real) *> : ( ( ) ( ) set ) & ex N being ( ( ) ( V160() V161() V162() ) Neighbourhood of x0 : ( ( ) ( V11() real ext-real ) Real) ) st
( N : ( ( ) ( V160() V161() V162() ) Neighbourhood of b₃ : ( ( ) ( V11() real ext-real ) Real) ) c= dom (SVF1 (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V160() V161() V162() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) & ex L being ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) ex R being ( ( V21() RestFunc-like ) ( V1() V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) st
for x being ( ( ) ( V11() real ext-real ) Real) st x : ( ( ) ( V11() real ext-real ) Real) in N : ( ( ) ( V160() V161() V162() ) Neighbourhood of b₃ : ( ( ) ( V11() real ext-real ) Real) ) holds
((SVF1 (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) - ((SVF1 (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . x0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) = (L : ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) . (x : ( ( ) ( V11() real ext-real ) Real) - x0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) + (R : ( ( V21() RestFunc-like ) ( V1() V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) . (x : ( ( ) ( V11() real ext-real ) Real) - x0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) );

pred f is_hpartial_differentiable`22_in u means :: PDIFF_5:def 5
ex x0, y0, z0 being ( ( ) ( V11() real ext-real ) Real) st
( u : ( ( ) ( ) set ) = <*x0 : ( ( ) ( V11() real ext-real ) Real) ,y0 : ( ( ) ( V11() real ext-real ) Real) ,z0 : ( ( ) ( V11() real ext-real ) Real) *> : ( ( ) ( ) set ) & ex N being ( ( ) ( V160() V161() V162() ) Neighbourhood of y0 : ( ( ) ( V11() real ext-real ) Real) ) st
( N : ( ( ) ( V160() V161() V162() ) Neighbourhood of b₃ : ( ( ) ( V11() real ext-real ) Real) ) c= dom (SVF1 (2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V160() V161() V162() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) & ex L being ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) ex R being ( ( V21() RestFunc-like ) ( V1() V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) st
for y being ( ( ) ( V11() real ext-real ) Real) st y : ( ( ) ( V11() real ext-real ) Real) in N : ( ( ) ( V160() V161() V162() ) Neighbourhood of b₃ : ( ( ) ( V11() real ext-real ) Real) ) holds
((SVF1 (2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) - ((SVF1 (2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . y0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) = (L : ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) . (y : ( ( ) ( V11() real ext-real ) Real) - y0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) + (R : ( ( V21() RestFunc-like ) ( V1() V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) . (y : ( ( ) ( V11() real ext-real ) Real) - y0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) );

pred f is_hpartial_differentiable`23_in u means :: PDIFF_5:def 6
ex x0, y0, z0 being ( ( ) ( V11() real ext-real ) Real) st
( u : ( ( ) ( ) set ) = <*x0 : ( ( ) ( V11() real ext-real ) Real) ,y0 : ( ( ) ( V11() real ext-real ) Real) ,z0 : ( ( ) ( V11() real ext-real ) Real) *> : ( ( ) ( ) set ) & ex N being ( ( ) ( V160() V161() V162() ) Neighbourhood of z0 : ( ( ) ( V11() real ext-real ) Real) ) st
( N : ( ( ) ( V160() V161() V162() ) Neighbourhood of b₃ : ( ( ) ( V11() real ext-real ) Real) ) c= dom (SVF1 (3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V160() V161() V162() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) & ex L being ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) ex R being ( ( V21() RestFunc-like ) ( V1() V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) st
for z being ( ( ) ( V11() real ext-real ) Real) st z : ( ( ) ( V11() real ext-real ) Real) in N : ( ( ) ( V160() V161() V162() ) Neighbourhood of b₃ : ( ( ) ( V11() real ext-real ) Real) ) holds
((SVF1 (3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . z : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) - ((SVF1 (3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( V21() ) ( V16() V19( REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( V1() V16() V19( REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative V136() V159() V160() V161() V162() V163() V164() V165() ) Element of NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() FinSequence-membered ) M11( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,u : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . z0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) = (L : ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) . (z : ( ( ) ( V11() real ext-real ) Real) - z0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) + (R : ( ( V21() RestFunc-like ) ( V1() V16() V19( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) . (z : ( ( ) ( V11() real ext-real ) Real) - z0 : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V54() V160() V161() V162() V166() ) set ) ) ) );