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

proof

let x be Element of X; :: thesis: H₁(x) in - Y
F . x in Y by FUNCT_2:7;
hence H₁(x) in - Y by Th23; :: thesis: verum

end;

ex H being Function of X,(- Y) 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) such that
A2: for x being Element of X holds H . x = - (F . x) ;
take H ; :: thesis: for x being Element of X holds H . x = - (F . x)
thus for x being Element of X holds H . x = - (F . x) by A2; :: thesis: verum