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 sequence of INT- such that
A2: for x being Element of NAT holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
A3: f in Funcs (NAT,INT-) by FUNCT_2:8;
then A4: dom f = NAT by FUNCT_2:92;
A5: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

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

end;

A9: for y being object st y in INT- holds
f " {y} <> {}

proof

let y be object ; :: thesis: ( y in INT- implies f " {y} <> {} )
assume A10: y in INT- ; :: thesis: f " {y} <> {}
then reconsider y = y as Real ;
consider k being Element of NAT such that
A11: y = - k by A10, Def1;
f . k = - k by A2;
then f . k in {y} by A11, TARSKI:def 1;
hence f " {y} <> {} by A4, FUNCT_1:def 7; :: thesis: verum

end;

A12: f is one-to-one by A5, FUNCT_1:def 4;
rng f = INT- by A9, FUNCT_2:41;
hence NAT , INT- are_equipotent by A4, A12, WELLORD2:def 4; :: thesis: verum