defpred S₁[ Element of NAT , set ] means $2 = - $1;
A1: for x being Element of NAT ex y being Element of INT- st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of INT- st S₁[x,y]
- x in INT- by Def1;
hence ex y being Element of INT- st S₁[x,y] ; :: thesis: verum

end;

consider f being Function of NAT,INT- such that
A3: for x being Element of NAT holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
A4: f in Funcs (NAT,INT-) by FUNCT_2:11;
then A5: dom f = NAT by FUNCT_2:169;
A6: for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A7: x1 in dom f and
A8: x2 in dom f and
A9: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x1 = x1 as Element of NAT by A4, A7, FUNCT_2:169;
reconsider x2 = x2 as Element of NAT by A4, A8, FUNCT_2:169;
( f . x1 = - x1 & f . x2 = - x2 ) by A3;
then - (- x1) = x2 by A9;
hence x1 = x2 ; :: thesis: verum

end;

A12: for y being set st y in INT- holds
f " {y} <> {}

proof

let y be set ; :: thesis: ( y in INT- implies f " {y} <> {} )
assume A13: y in INT- ; :: thesis: f " {y} <> {}
then reconsider y = y as Real ;
consider k being Element of NAT such that
A14: y = - k by A13, Def1;
f . k = - k by A3;
then f . k in {y} by A14, TARSKI:def 1;
hence f " {y} <> {} by A5, FUNCT_1:def 13; :: thesis: verum

end;

A17: f is one-to-one by A6, FUNCT_1:def 8;
rng f = INT- by A12, FUNCT_2:49;
hence NAT , INT- are_equipotent by A5, A17, WELLORD2:def 4; :: thesis: verum