let f be PartFunc of REAL,REAL; :: thesis: f + f = 2 (#) f
A1: dom (f + f) = (dom f) /\ (dom f) by VALUED_1:def 1
.= dom f ;
A2: dom (2 (#) f) = dom f by VALUED_1:def 5;

now :: thesis: for t being object st t in dom (f + f) holds
(f + f) . t = (2 (#) f) . t

let t be object ; :: thesis: ( t in dom (f + f) implies (f + f) . t = (2 (#) f) . t )
assume t in dom (f + f) ; :: thesis: (f + f) . t = (2 (#) f) . t
hence (f + f) . t = (f . t) + (f . t) by VALUED_1:def 1
.= 2 * (f . t)
.= (2 (#) f) . t by VALUED_1:6 ;
:: thesis: verum

end;

hence f + f = 2 (#) f by A1, A2, FUNCT_1:2; :: thesis: verum