deffunc H1( Element of X) -> R_eal = (F . $1) + (G . $1);
A1: for x being Element of X holds H1(x) in Y + Z
proof
let x be Element of X; :: thesis: H1(x) in Y + Z
A2: G . x in Z by FUNCT_2:5;
F . x in Y by FUNCT_2:5;
hence H1(x) in Y + Z by A2; :: thesis: verum
end;
ex H being Function of X,(Y + Z) st
for x being Element of X holds H . x = H1(x) from FUNCT_2:sch 8(A1);
 then consider H being Function of X,(Y + Z) such that
A3: for x being Element of X holds H . x = (F . x) + (G . x) ;
take H ; :: thesis: for x being Element of X holds H . x = (F . x) + (G . x)
thus for x being Element of X holds H . x = (F . x) + (G . x) by A3; :: thesis: verum