deffunc H₁( Element of X) -> Element of ExtREAL = (F . $1) + (G . $1);
A1: for x being Element of X holds H₁(x) in Y + Z

proof

let x be Element of X; :: thesis: H₁(x) in Y + Z
A2: G . x in Z by FUNCT_2:5;
F . x in Y by FUNCT_2:5;
hence H₁(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 = H₁(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