defpred S₁[ Element of BOOLEAN * , object ] means $2 = ExAbsval $1;
A1: for x being Element of BOOLEAN * ex y being Element of NAT st S₁[x,y]

proof

let x be Element of BOOLEAN * ; :: thesis: ex y being Element of NAT st S₁[x,y]
set y = ExAbsval x;
reconsider y = ExAbsval x as Element of NAT by ORDINAL1:def 12;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider f being Function of (BOOLEAN *),NAT such that
A2: for x being Element of BOOLEAN * holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for x being Element of BOOLEAN * holds f . x = ExAbsval x
thus for x being Element of BOOLEAN * holds f . x = ExAbsval x by A2; :: thesis: verum