:: CFDIFF_1 semantic presentation

begin

definition
let x be ( ( real ) ( V22() real ext-real ) number ) ;
let IT be ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ;
attr IT is x -convergent means :: CFDIFF_1:def 1
( IT : ( ( ext-real ) ( ext-real ) set ) is convergent & lim IT : ( ( ext-real ) ( ext-real ) set ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = x : ( ( ext-real ) ( ext-real ) set ) );
end;

theorem :: CFDIFF_1:1
for rs being ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence)
for cs being ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) st rs : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) = cs : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) & rs : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent holds
cs : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) is convergent ;

definition
let r be ( ( real ) ( V22() real ext-real ) number ) ;
func InvShift r -> ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) means :: CFDIFF_1:def 2
 for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) holds it : ( ( ext-real ) ( ext-real ) set ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = 1 : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) / (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) + r : ( ( ext-real ) ( ext-real ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) ;
end;

theorem :: CFDIFF_1:2
for r being ( ( real ) ( V22() real ext-real ) number ) st 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( real ) ( V22() real ext-real ) number ) holds
InvShift r : ( ( real ) ( V22() real ext-real ) number ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) is convergent ;

registration
let r be ( ( real positive ) ( V11() V22() real ext-real positive non negative ) number ) ;
cluster InvShift r : ( ( real positive ) ( V11() V22() real ext-real positive non negative ) set ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) -> Function-like quasi_total convergent ;
end;

theorem :: CFDIFF_1:3
for r being ( ( real ) ( V22() real ext-real ) number ) st 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( real ) ( V22() real ext-real ) number ) holds
lim (InvShift r : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ;

registration
let r be ( ( real positive ) ( V11() V22() real ext-real positive non negative ) number ) ;
cluster InvShift r : ( ( real positive ) ( V11() V22() real ext-real positive non negative ) set ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued bounded convergent ) Complex_Sequence) -> non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ;
end;

registration
cluster V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent for ( ( ) ( ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent -> Function-like quasi_total convergent for ( ( ) ( ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like constant V11() total quasi_total complex-valued for ( ( ) ( ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ;
end;

theorem :: CFDIFF_1:4
for seq being ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) holds
( seq : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) is constant iff for n, m being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) holds seq : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = seq : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) . m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ;

theorem :: CFDIFF_1:5
for seq being ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence)
for Nseq being ( ( Function-like quasi_total V37() ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V11() total quasi_total complex-valued ext-real-valued real-valued natural-valued V37() non-decreasing ) sequence of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) )
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) holds (seq : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) * Nseq : ( ( Function-like quasi_total V37() ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V11() total quasi_total complex-valued ext-real-valued real-valued natural-valued V37() non-decreasing ) sequence of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = seq : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) . (Nseq : ( ( Function-like quasi_total V37() ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like V11() total quasi_total complex-valued ext-real-valued real-valued natural-valued V37() non-decreasing ) sequence of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative ) Element of REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ;

definition
let IT be ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
attr IT is RestFunc-like means :: CFDIFF_1:def 3
 for h being ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued bounded convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) Complex_Sequence) holds
( (h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued bounded convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) Complex_Sequence) ") : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) (#) (IT : ( ( ) ( ) set ) /* h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued bounded convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) Complex_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) is convergent & lim ((h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued bounded convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) Complex_Sequence) ") : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) (#) (IT : ( ( ) ( ) set ) /* h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued bounded convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) Complex_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) );
end;

registration
cluster V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like total complex-valued RestFunc-like for ( ( ) ( ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ;
end;

definition
mode C_RestFunc is ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) PartFunc of ,) ;
end;

definition
let IT be ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
attr IT is linear means :: CFDIFF_1:def 4
 ex a being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st
for z being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) holds IT : ( ( ) ( ) set ) /. z : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = a : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) * z : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ;
end;

registration
cluster V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like total complex-valued linear for ( ( ) ( ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ;
end;

definition
mode C_LinearFunc is ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) PartFunc of ,) ;
end;

registration
let L1, L2 be ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) C_LinearFunc) ;
cluster L1 : ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) + L2 : ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( V1() Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like total complex-valued ) set ) -> Function-like total linear for ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
cluster L1 : ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) - L2 : ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( V1() Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like total complex-valued ) set ) -> Function-like total linear for ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
end;

registration
let a be ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ;
let L be ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) C_LinearFunc) ;
cluster a : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) (#) L : ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( V1() Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like total complex-valued ) set ) -> Function-like total linear for ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
end;

registration
let R1, R2 be ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) C_RestFunc) ;
cluster R1 : ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) + R2 : ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( V1() Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like total complex-valued ) set ) -> Function-like total RestFunc-like for ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
cluster R1 : ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) - R2 : ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( V1() Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like total complex-valued ) set ) -> Function-like total RestFunc-like for ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
cluster R1 : ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) (#) R2 : ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( V1() Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like total complex-valued ) set ) -> Function-like total RestFunc-like for ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
end;

registration
let a be ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ;
let R be ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) C_RestFunc) ;
cluster a : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) (#) R : ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( V1() Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like total complex-valued ) set ) -> Function-like total RestFunc-like for ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
end;

registration
let L1, L2 be ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) C_LinearFunc) ;
cluster L1 : ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) (#) L2 : ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( V1() Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like total complex-valued ) set ) -> Function-like total RestFunc-like for ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
end;

registration
let R be ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) C_RestFunc) ;
let L be ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) C_LinearFunc) ;
cluster R : ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) (#) L : ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( V1() Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like total complex-valued ) set ) -> Function-like total RestFunc-like for ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
cluster L : ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) (#) R : ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( V1() Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like total complex-valued ) set ) -> Function-like total RestFunc-like for ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
end;

definition
let z0 be ( ( V22() ) ( V22() ) Complex) ;
mode Neighbourhood of z0 -> ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) means :: CFDIFF_1:def 5
 ex g being ( ( ) ( V22() real ext-real ) Real) st
( 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) < g : ( ( ) ( V22() real ext-real ) Real) & { y : ( ( V22() ) ( V22() ) Complex) where y is ( ( V22() ) ( V22() ) Complex) : |.(y : ( ( V22() ) ( V22() ) Complex) - z0 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) .| : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) < g : ( ( ) ( V22() real ext-real ) Real) } c= it : ( ( V11() ) ( V11() ) set ) );
end;

theorem :: CFDIFF_1:6
for z0 being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) )
for g being ( ( real ) ( V22() real ext-real ) number ) st 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) < g : ( ( real ) ( V22() real ext-real ) number ) holds
{ y : ( ( V22() ) ( V22() ) Complex) where y is ( ( V22() ) ( V22() ) Complex) : |.(y : ( ( V22() ) ( V22() ) Complex) - z0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) set ) .| : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) < g : ( ( real ) ( V22() real ext-real ) number ) } is ( ( ) ( V45() ) Neighbourhood of z0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ;

theorem :: CFDIFF_1:7
for z0 being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) )
for N being ( ( ) ( V45() ) Neighbourhood of z0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) holds z0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in N : ( ( ) ( V45() ) Neighbourhood of b1 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ;

definition
let f be ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
let z0 be ( ( V22() ) ( V22() ) Complex) ;
pred f is_differentiable_in z0 means :: CFDIFF_1:def 6
 ex N being ( ( ) ( V45() ) Neighbourhood of z0 : ( ( V11() ) ( V11() ) set ) ) st
( N : ( ( ) ( V45() ) Neighbourhood of z0 : ( ( V22() ) ( V22() ) Complex) ) c= dom f : ( ( ) ( ) set ) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) & ex L being ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) C_LinearFunc) ex R being ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) C_RestFunc) st
for z being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st z : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in N : ( ( ) ( V45() ) Neighbourhood of z0 : ( ( V22() ) ( V22() ) Complex) ) holds
(f : ( ( ) ( ) set ) /. z : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) - (f : ( ( ) ( ) set ) /. z0 : ( ( V11() ) ( V11() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = (L : ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) C_LinearFunc) /. (z : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) - z0 : ( ( V11() ) ( V11() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) + (R : ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) C_RestFunc) /. (z : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) - z0 : ( ( V11() ) ( V11() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) );
end;

definition
let f be ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
let z0 be ( ( V22() ) ( V22() ) Complex) ;
assume f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_in z0 : ( ( V22() ) ( V22() ) Complex) ;
func diff (f,z0) -> ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) means :: CFDIFF_1:def 7
 ex N being ( ( ) ( V45() ) Neighbourhood of z0 : ( ( V11() ) ( V11() ) set ) ) st
( N : ( ( ) ( V45() ) Neighbourhood of z0 : ( ( V22() ) ( V22() ) Complex) ) c= dom f : ( ( ) ( ) set ) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) & ex L being ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) C_LinearFunc) ex R being ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) C_RestFunc) st
( it : ( ( ) ( ) set ) = L : ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) C_LinearFunc) /. 1r : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) & ( for z being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st z : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in N : ( ( ) ( V45() ) Neighbourhood of z0 : ( ( V22() ) ( V22() ) Complex) ) holds
(f : ( ( ) ( ) set ) /. z : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) - (f : ( ( ) ( ) set ) /. z0 : ( ( V11() ) ( V11() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = (L : ( ( Function-like total linear ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued linear ) C_LinearFunc) /. (z : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) - z0 : ( ( V11() ) ( V11() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) + (R : ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) C_RestFunc) /. (z : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) - z0 : ( ( V11() ) ( V11() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ) );
end;

definition
let f be ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
attr f is differentiable means :: CFDIFF_1:def 8
 for x being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in dom f : ( ( ) ( ) set ) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( ) ( ) set ) is_differentiable_in x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ;
end;

definition
let f be ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
let X be ( ( ) ( ) set ) ;
pred f is_differentiable_on X means :: CFDIFF_1:def 9
( X : ( ( V11() ) ( V11() ) set ) c= dom f : ( ( ) ( ) set ) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( ) ( ) set ) | X : ( ( V11() ) ( V11() ) set ) : ( ( ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) is differentiable );
end;

theorem :: CFDIFF_1:8
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) st f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) is ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) ;

definition
let X be ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) ;
attr X is closed means :: CFDIFF_1:def 10
 for s1 being ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) st rng s1 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) c= X : ( ( ) ( ) set ) & s1 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) is convergent holds
lim s1 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in X : ( ( ) ( ) set ) ;
end;

definition
let X be ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) ;
attr X is open means :: CFDIFF_1:def 11
X : ( ( ) ( ) set ) ` : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) is closed ;
end;

theorem :: CFDIFF_1:9
for X being ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) is open holds
for z0 being ( ( V22() ) ( V22() ) Complex) st z0 : ( ( V22() ) ( V22() ) Complex) in X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) holds
ex N being ( ( ) ( V45() ) Neighbourhood of z0 : ( ( V22() ) ( V22() ) Complex) ) st N : ( ( ) ( V45() ) Neighbourhood of b2 : ( ( V22() ) ( V22() ) Complex) ) c= X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) ;

theorem :: CFDIFF_1:10
for X being ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) st X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) is open holds
for z0 being ( ( V22() ) ( V22() ) Complex) st z0 : ( ( V22() ) ( V22() ) Complex) in X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) holds
ex g being ( ( ) ( V22() real ext-real ) Real) st { y : ( ( V22() ) ( V22() ) Complex) where y is ( ( V22() ) ( V22() ) Complex) : |.(y : ( ( V22() ) ( V22() ) Complex) - z0 : ( ( V22() ) ( V22() ) Complex) ) : ( ( ) ( V22() ) set ) .| : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) < g : ( ( ) ( V22() real ext-real ) Real) } c= X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) ;

theorem :: CFDIFF_1:11
for X being ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) st ( for z0 being ( ( V22() ) ( V22() ) Complex) st z0 : ( ( V22() ) ( V22() ) Complex) in X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) holds
ex N being ( ( ) ( V45() ) Neighbourhood of z0 : ( ( V22() ) ( V22() ) Complex) ) st N : ( ( ) ( V45() ) Neighbourhood of b2 : ( ( V22() ) ( V22() ) Complex) ) c= X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) ) holds
X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) is open ;

theorem :: CFDIFF_1:12
for X being ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) holds
( X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) is open iff for x being ( ( V22() ) ( V22() ) Complex) st x : ( ( V22() ) ( V22() ) Complex) in X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) holds
ex N being ( ( ) ( V45() ) Neighbourhood of x : ( ( V22() ) ( V22() ) Complex) ) st N : ( ( ) ( V45() ) Neighbourhood of b2 : ( ( V22() ) ( V22() ) Complex) ) c= X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) ) ;

theorem :: CFDIFF_1:13
for X being ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) )
for z0 being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) )
for r being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) st X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) = { y : ( ( V22() ) ( V22() ) Complex) where y is ( ( V22() ) ( V22() ) Complex) : |.(y : ( ( V22() ) ( V22() ) Complex) - z0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) set ) .| : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) < r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) } holds
X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) is open ;

theorem :: CFDIFF_1:14
for X being ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) )
for z0 being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) )
for r being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) st X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) = { y : ( ( V22() ) ( V22() ) Complex) where y is ( ( V22() ) ( V22() ) Complex) : |.(y : ( ( V22() ) ( V22() ) Complex) - z0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) set ) .| : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) <= r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) } holds
X : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) is closed ;

registration
cluster V45() open for ( ( ) ( ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ;
end;

theorem :: CFDIFF_1:15
for f being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for Z being ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
( f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) iff ( Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_in x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ) ) ;

theorem :: CFDIFF_1:16
for Y being ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) st f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on Y : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) holds
Y : ( ( ) ( V45() ) Subset of ( ( ) ( ) set ) ) is open ;

definition
let f be ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ;
let X be ( ( ) ( ) set ) ;
assume f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) ;
func f `| X -> ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) means :: CFDIFF_1:def 12
( dom it : ( ( ) ( ) set ) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) = X : ( ( V11() ) ( V11() ) set ) & ( for x being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in X : ( ( V11() ) ( V11() ) set ) holds
it : ( ( ) ( ) set ) /. x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = diff (f : ( ( ) ( ) set ) ,x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) );
end;

theorem :: CFDIFF_1:17
for f being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for Z being ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) st Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) & ex a1 being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st rng f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) = {a1 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) } : ( ( ) ( V45() ) set ) holds
( f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
(f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) `| Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /. x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = 0c : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ) ;

registration
let seq be ( ( non-zero Function-like quasi_total ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ;
let k be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative ) Nat) ;
cluster seq : ( ( non-zero Function-like quasi_total ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ^\ k : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative ) set ) : ( ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like total complex-valued ) set ) -> V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like total ;
end;

registration
let h be ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued bounded convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) Complex_Sequence) ;
let n be ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ;
cluster h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued bounded convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ^\ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like total ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like total complex-valued ) set ) -> Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent for ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ;
end;

theorem :: CFDIFF_1:18
for k being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) )
for seq, seq1 being ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) holds (seq : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) + seq1 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ^\ k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) subsequence of b2 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) + b3 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ) = (seq : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ^\ k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) subsequence of b2 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ) + (seq1 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ^\ k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) subsequence of b3 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: CFDIFF_1:19
for k being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) )
for seq, seq1 being ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) holds (seq : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) - seq1 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ^\ k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) subsequence of b2 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) - b3 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ) = (seq : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ^\ k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) subsequence of b2 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ) - (seq1 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ^\ k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) subsequence of b3 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: CFDIFF_1:20
for k being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) )
for seq being ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) holds (seq : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ") : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ^\ k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) subsequence of b2 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) " : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ) = (seq : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ^\ k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) subsequence of b2 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ) " : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: CFDIFF_1:21
for k being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) )
for seq, seq1 being ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) holds (seq : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) (#) seq1 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ^\ k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) subsequence of b2 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) (#) b3 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ) = (seq : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ^\ k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) subsequence of b2 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ) (#) (seq1 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ^\ k : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) subsequence of b3 : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Complex_Sequence) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: CFDIFF_1:22
for f being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for x0 being ( ( V22() ) ( V22() ) Complex)
for N being ( ( ) ( V45() ) Neighbourhood of x0 : ( ( V22() ) ( V22() ) Complex) ) st f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( V22() ) ( V22() ) Complex) & N : ( ( ) ( V45() ) Neighbourhood of b2 : ( ( V22() ) ( V22() ) Complex) ) c= dom f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) holds
for h being ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued bounded convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) Complex_Sequence)
for c being ( ( Function-like constant quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like constant V11() total quasi_total complex-valued ) Complex_Sequence) st rng c : ( ( Function-like constant quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like constant V11() total quasi_total complex-valued ) Complex_Sequence) : ( ( ) ( V12() V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) = {x0 : ( ( V22() ) ( V22() ) Complex) } : ( ( ) ( V45() ) set ) & rng (h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued bounded convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) Complex_Sequence) + c : ( ( Function-like constant quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like constant V11() total quasi_total complex-valued ) Complex_Sequence) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) c= N : ( ( ) ( V45() ) Neighbourhood of b2 : ( ( V22() ) ( V22() ) Complex) ) holds
( (h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued bounded convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) Complex_Sequence) ") : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) (#) ((f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /* (h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued bounded convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) Complex_Sequence) + c : ( ( Function-like constant quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like constant V11() total quasi_total complex-valued ) Complex_Sequence) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) - (f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /* c : ( ( Function-like constant quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like constant V11() total quasi_total complex-valued ) Complex_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) is convergent & diff (f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x0 : ( ( V22() ) ( V22() ) Complex) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = lim ((h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued bounded convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) Complex_Sequence) ") : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) (#) ((f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /* (h : ( ( non-zero Function-like quasi_total 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) ( V1() non-zero V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued bounded convergent 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V43() V44() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) -convergent ) Complex_Sequence) + c : ( ( Function-like constant quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like constant V11() total quasi_total complex-valued ) Complex_Sequence) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) - (f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /* c : ( ( Function-like constant quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like constant V11() total quasi_total complex-valued ) Complex_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued ) Element of K19(K20(NAT : ( ( ) ( V11() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of K19(REAL : ( ( ) ( V11() V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ;

theorem :: CFDIFF_1:23
for f1, f2 being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for x0 being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) & f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) holds
( f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_in x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) & diff ((f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = (diff (f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) )) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) + (diff (f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) )) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ;

theorem :: CFDIFF_1:24
for f1, f2 being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for x0 being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) & f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) holds
( f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_in x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) & diff ((f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = (diff (f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) )) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) - (diff (f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) )) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ;

theorem :: CFDIFF_1:25
for a being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) )
for f being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for x0 being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) holds
( a : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) (#) f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_in x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) & diff ((a : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) (#) f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = a : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) * (diff (f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) )) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ;

theorem :: CFDIFF_1:26
for f1, f2 being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for x0 being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) & f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) holds
( f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_in x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) & diff ((f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = ((f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /. x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) * (diff (f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) )) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) + ((f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /. x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) * (diff (f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) )) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ;

theorem :: CFDIFF_1:27
for f being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for Z being ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) st Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) | Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) = id Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) : ( ( total ) ( V1() V4(b2 : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) ) V5(b2 : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) ) Function-like one-to-one total quasi_total complex-valued ) Element of K19(K20(b2 : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) ,b2 : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) holds
( f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
(f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) `| Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /. x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = 1r : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ) ;

theorem :: CFDIFF_1:28
for f1, f2 being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for Z being ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) st Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) c= dom (f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) & f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) & f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
( f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
((f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) `| Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /. x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = (diff (f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) )) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) + (diff (f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) )) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ) ;

theorem :: CFDIFF_1:29
for f1, f2 being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for Z being ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) st Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) c= dom (f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) & f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) & f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
( f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
((f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) `| Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /. x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = (diff (f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) )) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) - (diff (f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) )) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ) ;

theorem :: CFDIFF_1:30
for a being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) )
for f being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for Z being ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) st Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) c= dom (a : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) (#) f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
( a : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) (#) f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
((a : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) (#) f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) `| Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /. x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = a : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) * (diff (f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) )) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ) ;

theorem :: CFDIFF_1:31
for f1, f2 being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for Z being ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) st Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) c= dom (f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) & f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) & f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
( f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
((f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) `| Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /. x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = ((f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /. x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) * (diff (f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) )) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) + ((f1 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /. x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) * (diff (f2 : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) ,x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) )) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ) ;

theorem :: CFDIFF_1:32
for f being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for Z being ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) st Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) | Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) Element of K19(K20(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ,COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( complex-valued ) set ) ) : ( ( ) ( ) set ) ) is constant holds
( f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
(f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) `| Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /. x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = 0c : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ) ;

theorem :: CFDIFF_1:33
for a, b being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) )
for f being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for Z being ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) st Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) : ( ( ) ( V45() ) Element of K19(COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /. x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = (a : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) * x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) + b : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) holds
( f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) in Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) holds
(f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) `| Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) /. x : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = a : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ) ;

theorem :: CFDIFF_1:34
for f being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for x0 being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) st f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) holds
f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_continuous_in x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ;

theorem :: CFDIFF_1:35
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) st f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_continuous_on X : ( ( ) ( ) set ) ;

theorem :: CFDIFF_1:36
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,)
for Z being ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) st f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) & Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) c= X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_on Z : ( ( open ) ( V45() open ) Subset of ( ( ) ( ) set ) ) ;

theorem :: CFDIFF_1:37
canceled;

theorem :: CFDIFF_1:38
for x0 being ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) )
for f being ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) st f : ( ( Function-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like complex-valued ) PartFunc of ,) is_differentiable_in x0 : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) holds
ex R being ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) C_RestFunc) st
( R : ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) C_RestFunc) /. 0c : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) = 0c : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) & R : ( ( Function-like total RestFunc-like ) ( V1() V4( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) V5( COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) Function-like V11() total quasi_total complex-valued RestFunc-like ) C_RestFunc) is_continuous_in 0c : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( V11() V45() V51() V52() ) set ) ) ) ;