:: FDIFF_1 semantic presentation

begin

theorem :: FDIFF_1:1
for Y being ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
( ( for r being ( ( ) ( V22() real ext-real ) Real) holds
( r : ( ( ) ( V22() real ext-real ) Real) in Y : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) iff r : ( ( ) ( V22() real ext-real ) Real) in REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) iff Y : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) = REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ;

definition
let x be ( ( real ) ( V22() real ext-real ) number ) ;
let IT be ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ;
attr IT is x -convergent means :: FDIFF_1:def 1
( IT : ( ( ext-real ) ( ext-real ) set ) is convergent & lim IT : ( ( ext-real ) ( ext-real ) set ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = x : ( ( ext-real ) ( ext-real ) set ) );
end;

registration
cluster V1() non-zero V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent for ( ( ) ( ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ;
end;

registration
let f be ( ( V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Real_Sequence) ;
cluster lim f : ( ( V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) : ( ( real ) ( V22() real ext-real ) set ) -> empty real ;
end;

registration
cluster V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent -> V6() quasi_total convergent for ( ( ) ( ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ;
end;

definition
let IT be ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
attr IT is RestFunc-like means :: FDIFF_1:def 2
( IT : ( ( V12() ) ( non empty V12() V74() ) set ) is total & ( for h being ( ( non-zero V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Real_Sequence) holds
( (h : ( ( non-zero V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Real_Sequence) ") : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) (#) (IT : ( ( V12() ) ( non empty V12() V74() ) set ) /* h : ( ( non-zero V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Real_Sequence) ) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is convergent & lim ((h : ( ( non-zero V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Real_Sequence) ") : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) (#) (IT : ( ( V12() ) ( non empty V12() V74() ) set ) /* h : ( ( non-zero V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Real_Sequence) ) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) ) ) );
end;

registration
cluster V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like for ( ( ) ( ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ;
end;

definition
mode RestFunc is ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) PartFunc of ,) ;
end;

definition
let IT be ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
attr IT is linear means :: FDIFF_1:def 3
( IT : ( ( V12() ) ( non empty V12() V74() ) set ) is total & ex r being ( ( ) ( V22() real ext-real ) Real) st
for p being ( ( ) ( V22() real ext-real ) Real) holds IT : ( ( V12() ) ( non empty V12() V74() ) set ) . p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = r : ( ( ) ( V22() real ext-real ) Real) * p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) );
end;

registration
cluster V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear for ( ( ) ( ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ;
end;

definition
mode LinearFunc is ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) PartFunc of ,) ;
end;

theorem :: FDIFF_1:2
for L1, L2 being ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) holds
( L1 : ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) + L2 : ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) & L1 : ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) - L2 : ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) ) ;

theorem :: FDIFF_1:3
for r being ( ( ) ( V22() real ext-real ) Real)
for L being ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) holds r : ( ( ) ( V22() real ext-real ) Real) (#) L : ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) ;

theorem :: FDIFF_1:4
for R1, R2 being ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) holds
( R1 : ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) + R2 : ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) & R1 : ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) - R2 : ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) & R1 : ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) (#) R2 : ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) ) ;

theorem :: FDIFF_1:5
for r being ( ( ) ( V22() real ext-real ) Real)
for R being ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) holds r : ( ( ) ( V22() real ext-real ) Real) (#) R : ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) ;

theorem :: FDIFF_1:6
for L1, L2 being ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) holds L1 : ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) (#) L2 : ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is RestFunc-like ;

theorem :: FDIFF_1:7
for R being ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc)
for L being ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) holds
( R : ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) (#) L : ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) & L : ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) (#) R : ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) ) ;

definition
let f be ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
let x0 be ( ( real ) ( V22() real ext-real ) number ) ;
pred f is_differentiable_in x0 means :: FDIFF_1:def 4
 ex N being ( ( ) ( open V57() V58() V59() ) Neighbourhood of x0 : ( ( non empty ) ( non empty ) set ) ) st
( N : ( ( ) ( open V57() V58() V59() ) Neighbourhood of x0 : ( ( real ) ( V22() real ext-real ) number ) ) c= dom f : ( ( V12() ) ( non empty V12() V74() ) set ) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) & ex L being ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) ex R being ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) st
for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in N : ( ( ) ( open V57() V58() V59() ) Neighbourhood of x0 : ( ( real ) ( V22() real ext-real ) number ) ) holds
(f : ( ( V12() ) ( non empty V12() V74() ) set ) . x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) - (f : ( ( V12() ) ( non empty V12() V74() ) set ) . x0 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = (L : ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) . (x : ( ( ) ( V22() real ext-real ) Real) - x0 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) + (R : ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) . (x : ( ( ) ( V22() real ext-real ) Real) - x0 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) );
end;

definition
let f be ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
let x0 be ( ( real ) ( V22() real ext-real ) number ) ;
assume f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( real ) ( V22() real ext-real ) number ) ;
func diff (f,x0) -> ( ( ) ( V22() real ext-real ) Real) means :: FDIFF_1:def 5
 ex N being ( ( ) ( open V57() V58() V59() ) Neighbourhood of x0 : ( ( non empty ) ( non empty ) set ) ) st
( N : ( ( ) ( open V57() V58() V59() ) Neighbourhood of x0 : ( ( real ) ( V22() real ext-real ) number ) ) c= dom f : ( ( V12() ) ( non empty V12() V74() ) set ) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) & ex L being ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) ex R being ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) st
( it : ( ( ) ( ) set ) = L : ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) . 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in N : ( ( ) ( open V57() V58() V59() ) Neighbourhood of x0 : ( ( real ) ( V22() real ext-real ) number ) ) holds
(f : ( ( V12() ) ( non empty V12() V74() ) set ) . x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) - (f : ( ( V12() ) ( non empty V12() V74() ) set ) . x0 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = (L : ( ( V6() linear ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued linear ) LinearFunc) . (x : ( ( ) ( V22() real ext-real ) Real) - x0 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) + (R : ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) . (x : ( ( ) ( V22() real ext-real ) Real) - x0 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) ) );
end;

definition
let f be ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
let X be ( ( ) ( ) set ) ;
pred f is_differentiable_on X means :: FDIFF_1:def 6
( X : ( ( non empty ) ( non empty ) set ) c= dom f : ( ( V12() ) ( non empty V12() V74() ) set ) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in X : ( ( non empty ) ( non empty ) set ) holds
f : ( ( V12() ) ( non empty V12() V74() ) set ) | X : ( ( non empty ) ( non empty ) set ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is_differentiable_in x : ( ( ) ( V22() real ext-real ) Real) ) );
end;

theorem :: FDIFF_1:8
for X being ( ( ) ( ) set )
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) is ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ;

theorem :: FDIFF_1:9
for Z being ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) )
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) iff ( Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_in x : ( ( ) ( V22() real ext-real ) Real) ) ) ) ;

theorem :: FDIFF_1:10
for Y being ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) )
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Y : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
Y : ( ( ) ( V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) is open ;

definition
let f be ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
let X be ( ( ) ( ) set ) ;
assume f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) ;
func f `| X -> ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) means :: FDIFF_1:def 7
( dom it : ( ( ) ( ) set ) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) = X : ( ( non empty ) ( non empty ) set ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in X : ( ( non empty ) ( non empty ) set ) holds
it : ( ( ) ( ) set ) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = diff (f : ( ( V12() ) ( non empty V12() V74() ) set ) ,x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Real) ) );
end;

theorem :: FDIFF_1:11
for Z being ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) )
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) & ex r being ( ( ) ( V22() real ext-real ) Real) st rng f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) = {r : ( ( ) ( V22() real ext-real ) Real) } : ( ( ) ( non empty V12() V57() V58() V59() V64() V78(1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) ) ) set ) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
(f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) `| Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) ) ) ;

registration
let h be ( ( non-zero V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Real_Sequence) ;
let n be ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) ;
cluster h : ( ( non-zero V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ^\ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V6() total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() total complex-valued ext-real-valued real-valued ) set ) -> non-zero V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent for ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ;
end;

theorem :: FDIFF_1:12
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,)
for x0 being ( ( real ) ( V22() real ext-real ) number )
for N being ( ( ) ( open V57() V58() V59() ) Neighbourhood of x0 : ( ( real ) ( V22() real ext-real ) number ) ) st f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( real ) ( V22() real ext-real ) number ) & N : ( ( ) ( open V57() V58() V59() ) Neighbourhood of b2 : ( ( real ) ( V22() real ext-real ) number ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
for h being ( ( non-zero V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Real_Sequence)
for c being ( ( V6() V8() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() V8() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ) Real_Sequence) st rng c : ( ( V6() V8() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() V8() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ) Real_Sequence) : ( ( ) ( non empty V12() V57() V58() V59() V64() V78(1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) ) ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) = {x0 : ( ( real ) ( V22() real ext-real ) number ) } : ( ( ) ( non empty V12() V57() V58() V59() V64() V78(1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) ) ) set ) & rng (h : ( ( non-zero V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Real_Sequence) + c : ( ( V6() V8() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() V8() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ) Real_Sequence) ) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) : ( ( ) ( non empty V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) c= N : ( ( ) ( open V57() V58() V59() ) Neighbourhood of b2 : ( ( real ) ( V22() real ext-real ) number ) ) holds
( (h : ( ( non-zero V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Real_Sequence) ") : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) (#) ((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) /* (h : ( ( non-zero V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Real_Sequence) + c : ( ( V6() V8() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() V8() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ) Real_Sequence) ) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) - (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) /* c : ( ( V6() V8() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() V8() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ) Real_Sequence) ) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is convergent & diff (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Real) = lim ((h : ( ( non-zero V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Real_Sequence) ") : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) (#) ((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) /* (h : ( ( non-zero V6() quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) -convergent ) Real_Sequence) + c : ( ( V6() V8() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() V8() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ) Real_Sequence) ) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) - (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) /* c : ( ( V6() V8() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() V8() non empty total quasi_total complex-valued ext-real-valued real-valued convergent ) Real_Sequence) ) : ( ( V6() quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V6() ) ( V1() V4( NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of K19(K20(NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) ;

theorem :: FDIFF_1:13
for x0 being ( ( ) ( V22() real ext-real ) Real)
for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() real ext-real ) Real) & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() real ext-real ) Real) holds
( f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is_differentiable_in x0 : ( ( ) ( V22() real ext-real ) Real) & diff ((f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,x0 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Real) = (diff (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Real) + (diff (f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) ;

theorem :: FDIFF_1:14
for x0 being ( ( ) ( V22() real ext-real ) Real)
for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() real ext-real ) Real) & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() real ext-real ) Real) holds
( f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is_differentiable_in x0 : ( ( ) ( V22() real ext-real ) Real) & diff ((f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,x0 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Real) = (diff (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Real) - (diff (f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) ;

theorem :: FDIFF_1:15
for x0, r being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() real ext-real ) Real) holds
( r : ( ( ) ( V22() real ext-real ) Real) (#) f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is_differentiable_in x0 : ( ( ) ( V22() real ext-real ) Real) & diff ((r : ( ( ) ( V22() real ext-real ) Real) (#) f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,x0 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Real) = r : ( ( ) ( V22() real ext-real ) Real) * (diff (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) ;

theorem :: FDIFF_1:16
for x0 being ( ( ) ( V22() real ext-real ) Real)
for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() real ext-real ) Real) & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() real ext-real ) Real) holds
( f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is_differentiable_in x0 : ( ( ) ( V22() real ext-real ) Real) & diff ((f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ,x0 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Real) = ((f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) * (diff (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) + ((f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) * (diff (f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) ;

theorem :: FDIFF_1:17
for Z being ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) )
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) : ( ( V6() ) ( V1() V4(b1 : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) = id Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) : ( ( V6() ) ( V1() V4(b1 : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5(b1 : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() V7() total complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
(f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) `| Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) ) ) ;

theorem :: FDIFF_1:18
for Z being ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) )
for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) c= dom (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) & f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
( f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
((f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) `| Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = (diff (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Real) + (diff (f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) ) ;

theorem :: FDIFF_1:19
for Z being ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) )
for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) c= dom (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) & f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
( f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
((f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) `| Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = (diff (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Real) - (diff (f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) ) ;

theorem :: FDIFF_1:20
for r being ( ( ) ( V22() real ext-real ) Real)
for Z being ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) )
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) c= dom (r : ( ( ) ( V22() real ext-real ) Real) (#) f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
( r : ( ( ) ( V22() real ext-real ) Real) (#) f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
((r : ( ( ) ( V22() real ext-real ) Real) (#) f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) `| Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = r : ( ( ) ( V22() real ext-real ) Real) * (diff (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) ) ;

theorem :: FDIFF_1:21
for Z being ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) )
for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) c= dom (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) & f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
( f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
((f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) `| Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = ((f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) * (diff (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) + ((f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) * (diff (f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) ) ;

theorem :: FDIFF_1:22
for Z being ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) )
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) : ( ( V6() ) ( V1() V4(b1 : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ) V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is V8() holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
(f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) `| Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) ) ) ;

theorem :: FDIFF_1:23
for r, p being ( ( ) ( V22() real ext-real ) Real)
for Z being ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) )
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = (r : ( ( ) ( V22() real ext-real ) Real) * x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) + p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) ) holds
( f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
(f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) `| Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = r : ( ( ) ( V22() real ext-real ) Real) ) ) ;

theorem :: FDIFF_1:24
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,)
for x0 being ( ( real ) ( V22() real ext-real ) number ) st f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( real ) ( V22() real ext-real ) number ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) ;

theorem :: FDIFF_1:25
for X being ( ( ) ( ) set )
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( V6() ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) is continuous ;

theorem :: FDIFF_1:26
for X being ( ( ) ( ) set )
for Z being ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) )
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) & Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) c= X : ( ( ) ( ) set ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ;

theorem :: FDIFF_1:27
ex R being ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) st
( R : ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) . 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) & R : ( ( V6() RestFunc-like ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued RestFunc-like ) RestFunc) is_continuous_in 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V55() V56() V57() V58() V59() V60() V61() V62() V64() V76() ) Element of NAT : ( ( ) ( non empty V12() epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() V64() V74() V76() V77() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ) ) ;

definition
let f be ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
attr f is differentiable means :: FDIFF_1:def 8
f : ( ( V12() ) ( non empty V12() V74() ) set ) is_differentiable_on dom f : ( ( V12() ) ( non empty V12() V74() ) set ) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ;
end;

registration
cluster V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued differentiable for ( ( ) ( ) Element of K19(K20(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ,REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( V1() non empty V12() complex-valued ext-real-valued real-valued V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) ;
end;

theorem :: FDIFF_1:28
for Z being ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) )
for f being ( ( V6() differentiable ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued differentiable ) PartFunc of ,) st Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) c= dom f : ( ( V6() differentiable ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued differentiable ) PartFunc of ,) : ( ( ) ( V57() V58() V59() ) Element of K19(REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) : ( ( ) ( non empty V12() V64() V74() ) set ) ) holds
f : ( ( V6() differentiable ) ( V1() V4( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V5( REAL : ( ( ) ( non empty V12() V57() V58() V59() V63() V64() V74() ) set ) ) V6() complex-valued ext-real-valued real-valued differentiable ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( open V57() V58() V59() ) Subset of ( ( ) ( non empty V12() V64() V74() ) set ) ) ;