consider r2 being Element of REAL such that
A1: for c being Element of C st c in dom f2 holds
f2 . c = r2 by PARTFUN2:def 1;
consider r1 being Element of REAL such that
A2: for c being Element of C st c in dom f1 holds
f1 . c = r1 by PARTFUN2:def 1;
now :: thesis: for c being Element of C st c in dom (f1 + f2) holds
(f1 + f2) . c = r1 + r2
let c be Element of C; :: thesis: ( c in dom (f1 + f2) implies (f1 + f2) . c = r1 + r2 )
assume A3: c in dom (f1 + f2) ; :: thesis: (f1 + f2) . c = r1 + r2
then A4: c in (dom f1) /\ (dom f2) by VALUED_1:def 1;
then A5: c in dom f1 by XBOOLE_0:def 4;
A6: c in dom f2 by A4, XBOOLE_0:def 4;
thus (f1 + f2) . c = (f1 . c) + (f2 . c) by A3, VALUED_1:def 1
.= (f1 . c) + r2 by A1, A6
.= r1 + r2 by A2, A5 ; :: thesis: verum
end;
hence f1 + f2 is constant by PARTFUN2:def 1; :: thesis: verum