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

defpred S_{1}[ Element of A, set ] means $2 = H_{1}($1);

A1: for x being Element of A ex y being Element of B st S_{1}[x,y]

A2: for x being Element of A holds S_{1}[x,F . x]
from FUNCT_2:sch 3(A1);

take F ; :: thesis: for p being Element of A holds F . p = (F . p) . p

thus for p being Element of A holds F . p = (F . p) . p by A2; :: thesis: verum

defpred S

A1: for x being Element of A ex y being Element of B st S

proof

consider F being Function of A,B such that
let x be Element of A; :: thesis: ex y being Element of B st S_{1}[x,y]

reconsider Funx = F . x as Function of A,B by FUNCT_2:66;

Funx . x in B ;

hence ex y being Element of B st S_{1}[x,y]
; :: thesis: verum

end;reconsider Funx = F . x as Function of A,B by FUNCT_2:66;

Funx . x in B ;

hence ex y being Element of B st S

A2: for x being Element of A holds S

take F ; :: thesis: for p being Element of A holds F . p = (F . p) . p

thus for p being Element of A holds F . p = (F . p) . p by A2; :: thesis: verum