let R1 be REST; :: thesis: - R1 is REST
A1: R1 is total by FDIFF_1:def 3;
then A2: - R1 is total ;
A3: ( dom R1 = REAL & dom (- R1) = REAL ) by A1, PARTFUN1:def 4;
A4: for h being convergent_to_0 Real_Sequence holds - (R1 /* h) = (- R1) /* h

proof

let h be convergent_to_0 Real_Sequence; :: thesis: - (R1 /* h) = (- R1) /* h
rng h c= dom R1 by A3, VALUED_0:def 3;
hence - (R1 /* h) = (- R1) /* h by RFUNCT_2:25; :: thesis: verum

end;

now

let h be convergent_to_0 Real_Sequence; :: thesis: ( (h " ) (#) ((- R1) /* h) is convergent & lim ((h " ) (#) ((- R1) /* h)) = 0 )
A5: ( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0 ) by FDIFF_1:def 3;
A6: (h " ) (#) ((- R1) /* h) = (h " ) (#) (- (R1 /* h)) by A4
.= - ((h " ) (#) (R1 /* h)) by SEQ_1:27 ;
hence (h " ) (#) ((- R1) /* h) is convergent by A5, SEQ_2:23; :: thesis: lim ((h " ) (#) ((- R1) /* h)) = 0
thus lim ((h " ) (#) ((- R1) /* h)) = - (lim ((h " ) (#) (R1 /* h))) by A5, A6, SEQ_2:24
.= 0 by A5 ; :: thesis: verum

end;

hence - R1 is REST by A2, FDIFF_1:def 3; :: thesis: verum