let f be Function of REAL,REAL; :: thesis: f - f = REAL --> 0
reconsider g = REAL --> 0 as Function of REAL,REAL by XREAL_0:def 1, FUNCOP_1:45;
A1: dom (f - f) = REAL by FUNCT_2:def 1;
for x being object st x in REAL holds
(f - f) . x = g . x

proof

let x be object ; :: thesis: ( x in REAL implies (f - f) . x = g . x )
assume A2: x in REAL ; :: thesis: (f - f) . x = g . x
then (f - f) . x = (f . x) - (f . x) by A1, VALUED_1:13
.= (REAL --> 0) . x by A2, FUNCOP_1:7 ;
hence (f - f) . x = g . x ; :: thesis: verum

end;

hence f - f = REAL --> 0 ; :: thesis: verum