let n be Nat; :: thesis:
defpred S₁[ Element of INT , set ] means $2 = $1 / (n + 1);
A1: for x being Element of INT ex y being Element of RAT_with_denominator (n + 1) st S₁[x,y]

let x be Element of INT ; :: thesis:
reconsider x = x as Integer ;
reconsider i1 = n + 1 as Integer ;
set y = x / i1;
x / i1 in RAT by RAT_1:def 1;
then reconsider y = x / i1 as Rational ;
y in RAT_with_denominator (n + 1) by Def2;
hence ex y being Element of RAT_with_denominator (n + 1) st S₁[x,y] ; :: thesis:

end;

let x1, x2 be set ; :: thesis:
assume that
A8: x1 in dom f and
A9: x2 in dom f and
A10: f . x1 = f . x2 ; :: thesis:
reconsider x1 = x1 as Element of INT by A5, A8, FUNCT_2:169;
reconsider x2 = x2 as Element of INT by A5, A9, FUNCT_2:169;
( f . x1 = x1 / (n + 1) & f . x2 = x2 / (n + 1) ) by A4;
hence x1 = x2 by A10, XCMPLX_1:53; :: thesis:

end;

let y be set ; :: thesis:
assume A13: y in RAT_with_denominator (n + 1) ; :: thesis:
then reconsider y = y as Rational ;
consider i being Integer such that
A14: y = i / (n + 1) by A13, Def2;
reconsider i = i as Element of INT by INT_1:def 2;
f . i = i / (n + 1) by A4;
then f . i in {y} by A14, TARSKI:def 1;
hence f " {y} <> {} by A6, FUNCT_1:def 13; :: thesis:

end;