reconsider cf = COMPLEX --> 0c as Function of COMPLEX,COMPLEX ;
take f = cf; :: thesis: ( f is total & f is RestFunc-like )
thus f is total ; :: thesis: f is RestFunc-like
let h be non-zero 0 -convergent Complex_Sequence; :: according to CFDIFF_1:def 3 :: thesis: ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 )
now :: thesis: for n being Nat holds ((h ") (#) (f /* h)) . n = 0c
let n be Nat; :: thesis: ((h ") (#) (f /* h)) . n = 0c
A1: ( n in NAT & rng h c= dom f ) by ORDINAL1:def 12;
thus ((h ") (#) (f /* h)) . n = ((h ") . n) * ((f /* h) . n) by VALUED_1:5
.= ((h ") . n) * (f /. (h . n)) by A1, FUNCT_2:108
.= ((h ") . n) * 0c
.= 0c ; :: thesis: verum
end;
then ( (h ") (#) (f /* h) is constant & ((h ") (#) (f /* h)) . 0 = 0c ) by VALUED_0:def 18;
hence ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0c ) by CFCONT_1:26, CFCONT_1:27; :: thesis: verum