let R1 be RestFunc; :: thesis: - R1 is RestFunc
A1: R1 is total by FDIFF_1:def 2;
then A2: dom R1 = REAL by PARTFUN1:def 2;
A3: for h being non-zero 0 -convergent Real_Sequence holds - (R1 /* h) = (- R1) /* h

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: - (R1 /* h) = (- R1) /* h
rng h c= dom R1 by A2, VALUED_0:def 3;
hence - (R1 /* h) = (- R1) /* h by RFUNCT_2:10; :: thesis: verum

end;

now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) ((- R1) /* h) is convergent & lim ((h ") (#) ((- R1) /* h)) = 0 )

let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) ((- R1) /* h) is convergent & lim ((h ") (#) ((- R1) /* h)) = 0 )
A4: (h ") (#) (R1 /* h) is convergent by FDIFF_1:def 2;
A5: (h ") (#) ((- R1) /* h) = (h ") (#) (- (R1 /* h)) by A3
.= - ((h ") (#) (R1 /* h)) by SEQ_1:19 ;
hence (h ") (#) ((- R1) /* h) is convergent by A4, SEQ_2:9; :: thesis: lim ((h ") (#) ((- R1) /* h)) = 0
A6: lim ((h ") (#) (R1 /* h)) = 0 by FDIFF_1:def 2;
thus lim ((h ") (#) ((- R1) /* h)) = - (lim ((h ") (#) (R1 /* h))) by A4, A5, SEQ_2:10
.= 0 by A6 ; :: thesis: verum

end;

hence - R1 is RestFunc by A1, FDIFF_1:def 2; :: thesis: verum