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

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

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) 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

A1: for x being Element of X holds H

proof

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

F . x in Y by FUNCT_2:5;

hence H_{1}(x) in - Y
; :: thesis: verum

end;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) 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