deffunc H_{1}( Element of X) -> R_eal = (F . $1) + (G . $1);

A1: for x being Element of X holds H_{1}(x) in Y + Z

for x being Element of X holds H . x = H_{1}(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

A1: for x being Element of X holds H

proof

ex H being Function of X,(Y + Z) st
let x be Element of X; :: thesis: H_{1}(x) in Y + Z

A2: G . x in Z by FUNCT_2:5;

F . x in Y by FUNCT_2:5;

hence H_{1}(x) in Y + Z
by A2; :: thesis: verum

end;A2: G . x in Z by FUNCT_2:5;

F . x in Y by FUNCT_2:5;

hence H

for x being Element of X holds H . x = H

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