let A be non empty set ; :: thesis: for f, g being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,g) = f + g
let f, g be Element of Funcs (A,REAL); :: thesis: (RealFuncAdd A) . (f,g) = f + g
A1: dom ((RealFuncAdd A) . (f,g)) = A by FUNCT_2:def 1;
a1: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1
.= A /\ (dom g) by FUNCT_2:def 1
.= A /\ A by FUNCT_2:def 1
.= A ;

now :: thesis: for x being object st x in dom (f + g) holds
((RealFuncAdd A) . (f,g)) . x = (f + g) . x

let x be object ; :: thesis: ( x in dom (f + g) implies ((RealFuncAdd A) . (f,g)) . x = (f + g) . x )
assume a0: x in dom (f + g) ; :: thesis: ((RealFuncAdd A) . (f,g)) . x = (f + g) . x
A3: dom (addreal .: (f,g)) = A by FUNCT_2:def 1;
thus ((RealFuncAdd A) . (f,g)) . x = (addreal .: (f,g)) . x by Def1
.= addreal . ((f . x),(g . x)) by a1, a0, A3, FUNCOP_1:22
.= (f . x) + (g . x) by BINOP_2:def 9
.= (f + g) . x by VALUED_1:1, a1, a0 ; :: thesis: verum

end;

hence (RealFuncAdd A) . (f,g) = f + g by a1, A1, FUNCT_1:2; :: thesis: verum