deffunc H₁( Element of A) -> set = (F . $1) . $1;
defpred S₁[ Element of A, set ] means $2 = H₁($1);
A1: for x being Element of A ex y being Element of B st S₁[x,y]

proof

let x be Element of A; :: thesis: ex y being Element of B st S₁[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₁[x,y] ; :: thesis: verum

end;

consider F being Function of A,B such that
A2: for x being Element of A holds S₁[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