defpred S_{1}[ Element of RAT , Element of NAT ] means $2 = denominator $1;

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

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

take f ; :: thesis: for x being Rational holds f . x = denominator x

let x be Rational; :: thesis: f . x = denominator x

x in RAT by RAT_1:def 2;

hence f . x = denominator x by A2; :: thesis: verum

A1: for x being Element of RAT ex y being Element of NAT st S

proof

consider f being Function of RAT,NAT such that
let x be Element of RAT ; :: thesis: ex y being Element of NAT st S_{1}[x,y]

denominator x in NAT by ORDINAL1:def 12;

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

end;denominator x in NAT by ORDINAL1:def 12;

hence ex y being Element of NAT st S

A2: for x being Element of RAT holds S

take f ; :: thesis: for x being Rational holds f . x = denominator x

let x be Rational; :: thesis: f . x = denominator x

x in RAT by RAT_1:def 2;

hence f . x = denominator x by A2; :: thesis: verum