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 object ; :: thesis:
assume that
A6: x1 in dom f and
A7: x2 in dom f and
A8: f . x1 = f . x2 ; :: thesis:
reconsider x1 = x1 as Element of INT by A3, A6, FUNCT_2:92;
reconsider x2 = x2 as Element of INT by A3, A7, FUNCT_2:92;
( f . x1 = x1 / (n + 1) & f . x2 = x2 / (n + 1) ) by A2;
hence x1 = x2 by A8, XCMPLX_1:53; :: thesis:

end;

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

end;