let f be Function of REAL,REAL; :: thesis: 0 (#) f = REAL --> 0
for x being Element of REAL holds (0 (#) f) . x = (REAL --> 0) . x

proof

let x be Element of REAL ; :: thesis: (0 (#) f) . x = (REAL --> 0) . x
(0 (#) f) . x = 0 * (f . x) by RFUNCT_1:57;
hence (0 (#) f) . x = (REAL --> 0) . x ; :: thesis: verum

end;

hence 0 (#) f = REAL --> 0 ; :: thesis: verum