cluster V21() RestFunc-like -> V21() total RestFunc-like for ( ( ) ( ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ;

func pdiff1 (f,i) -> ( ( V21() quasi_total ) ( non empty V16() V19( REAL n : ( ( ) ( ) set ) : ( ( ) ( ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL n : ( ( ) ( ) set ) : ( ( ) ( ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) means :: PDIFF_3:def 1
for z being ( ( ) ( V16() V19( NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued V61(n : ( ( ) ( ) set ) ) FinSequence-like ) Element of REAL n : ( ( ) ( ) set ) : ( ( ) ( ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) holds it : ( ( ) ( V61(i : ( ( ) ( ) set ) ) ) Element of REAL i : ( ( ) ( ) set ) : ( ( ) ( ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) . z : ( ( ) ( V16() V19( NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued V61(n : ( ( non empty ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) Element of REAL n : ( ( non empty ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) = partdiff (f : ( ( V21() ) ( V16() V19( REAL i : ( ( ) ( ) set ) : ( ( ) ( ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL i : ( ( ) ( ) set ) ) : ( ( ) ( ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ,z : ( ( ) ( V16() V19( NAT : ( ( ) ( V160() V161() V162() V163() V164() V165() V166() ) Element of K6(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued V61(n : ( ( non empty ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) Element of REAL n : ( ( non empty ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) ,i : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ;

pred f is_hpartial_differentiable`11_in z means :: PDIFF_3:def 2
ex x0, y0 being ( ( ) ( V11() real ext-real ) Real) st
( z : ( ( ) ( ) set ) = <*x0 : ( ( ) ( V11() real ext-real ) Real) ,y0 : ( ( ) ( 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 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V160() V161() V162() ) Element of K6(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) & ex L being ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) ex R being ( ( V21() RestFunc-like ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() 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 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) - ((SVF1 (1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) = (L : ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) + (R : ( ( V21() RestFunc-like ) ( non empty V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) );

pred f is_hpartial_differentiable`12_in z means :: PDIFF_3:def 3
ex x0, y0 being ( ( ) ( V11() real ext-real ) Real) st
( z : ( ( ) ( ) set ) = <*x0 : ( ( ) ( V11() real ext-real ) Real) ,y0 : ( ( ) ( 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 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V160() V161() V162() ) Element of K6(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) & ex L being ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) ex R being ( ( V21() RestFunc-like ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() 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 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) - ((SVF1 (2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) = (L : ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) + (R : ( ( V21() RestFunc-like ) ( non empty V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) );

pred f is_hpartial_differentiable`21_in z means :: PDIFF_3:def 4
ex x0, y0 being ( ( ) ( V11() real ext-real ) Real) st
( z : ( ( ) ( ) set ) = <*x0 : ( ( ) ( V11() real ext-real ) Real) ,y0 : ( ( ) ( 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 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V160() V161() V162() ) Element of K6(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) & ex L being ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) ex R being ( ( V21() RestFunc-like ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() 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 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) - ((SVF1 (1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) = (L : ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) + (R : ( ( V21() RestFunc-like ) ( non empty V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) );

pred f is_hpartial_differentiable`22_in z means :: PDIFF_3:def 5
ex x0, y0 being ( ( ) ( V11() real ext-real ) Real) st
( z : ( ( ) ( ) set ) = <*x0 : ( ( ) ( V11() real ext-real ) Real) ,y0 : ( ( ) ( 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 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V160() V161() V162() ) Element of K6(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) & ex L being ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) ex R being ( ( V21() RestFunc-like ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() 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 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) - ((SVF1 (2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) = (L : ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) + (R : ( ( V21() RestFunc-like ) ( non empty V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) );

func hpartdiff11 (f,z) -> ( ( ) ( V11() real ext-real ) Real) means :: PDIFF_3:def 6
ex x0, y0 being ( ( ) ( V11() real ext-real ) Real) st
( z : ( ( ) ( ) set ) = <*x0 : ( ( ) ( V11() real ext-real ) Real) ,y0 : ( ( ) ( 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 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V160() V161() V162() ) Element of K6(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) & ex L being ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) ex R being ( ( V21() RestFunc-like ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) st
( it : ( ( V21() ) ( V16() V19( REAL f : ( ( ) ( ) set ) : ( ( ) ( ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL f : ( ( ) ( ) set ) ) : ( ( ) ( ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) = L : ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) . 1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) & ( 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 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) - ((SVF1 (1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) = (L : ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) + (R : ( ( V21() RestFunc-like ) ( non empty V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) ) ) );

func hpartdiff12 (f,z) -> ( ( ) ( V11() real ext-real ) Real) means :: PDIFF_3:def 7
ex x0, y0 being ( ( ) ( V11() real ext-real ) Real) st
( z : ( ( ) ( ) set ) = <*x0 : ( ( ) ( V11() real ext-real ) Real) ,y0 : ( ( ) ( 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 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V160() V161() V162() ) Element of K6(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) & ex L being ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) ex R being ( ( V21() RestFunc-like ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) st
( it : ( ( V21() ) ( V16() V19( REAL f : ( ( ) ( ) set ) : ( ( ) ( ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7((REAL f : ( ( ) ( ) set ) ) : ( ( ) ( ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ,REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) = L : ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued linear ) LinearFunc) . 1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) & ( 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 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) - ((SVF1 (2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) ,(pdiff1 (f : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( V21() quasi_total ) ( non empty V16() V19( REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL 2 : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty FinSequence-membered ) M11( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) )) , REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ,z : ( ( ) ( ) set ) )) : ( ( V21() ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V21() complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ,REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) = (L : ( ( V21() linear ) ( V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) + (R : ( ( V21() RestFunc-like ) ( non empty V16() V19( REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) V20( REAL : ( ( ) ( non empty 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 : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V54() V160() V161() V162() V166() ) set ) ) ) ) ) );