deffunc H₁( object , object ) -> object = [{$2},{}];
consider f1 being Function such that
A1: ( dom f1 = NAT & f1 . 0 = 0_No ) and
A2: for n being Nat holds f1 . (n + 1) = H₁(n,f1 . n) from NAT_1:sch 11();
deffunc H₂( object , object ) -> object = [{},{$2}];
consider f2 being Function such that
A3: ( dom f2 = NAT & f2 . 0 = 0_No ) and
A4: for n being Nat holds f2 . (n + 1) = H₂(n,f2 . n) from NAT_1:sch 11();
defpred S₁[ object , object ] means for i being Integer st i = $1 holds
( ( i >= 0 implies $2 = f1 . i ) & ( i < 0 implies $2 = f2 . (- i) ) );
A5: for i being object st i in INT holds
ex j being object st S₁[i,j]

proof

let i be object ; :: thesis: ( i in INT implies ex j being object st S₁[i,j] )
assume i in INT ; :: thesis: ex j being object st S₁[i,j]
then reconsider x = i as Integer ;

per cases ( x >= 0 or x < 0 ) ;

suppose A6: x >= 0 ; :: thesis: ex j being object st S₁[i,j]

take f1 . x ; :: thesis: S₁[i,f1 . x]
thus S₁[i,f1 . x] by A6; :: thesis: verum

end;

suppose A7: x < 0 ; :: thesis: ex j being object st S₁[i,j]

take f2 . (- x) ; :: thesis: S₁[i,f2 . (- x)]
thus S₁[i,f2 . (- x)] by A7; :: thesis: verum

end;

end;

end;

consider f being ManySortedSet of INT such that
A8: for i being object st i in INT holds
S₁[i,f . i] from PBOOLE:sch 3(A5);
take f ; :: thesis: for n being Nat holds
( f . 0 = 0_No & f . (n + 1) = [{(f . n)},{}] & f . (- (n + 1)) = [{},{(f . (- n))}] )
let n be Nat; :: thesis: ( f . 0 = 0_No & f . (n + 1) = [{(f . n)},{}] & f . (- (n + 1)) = [{},{(f . (- n))}] )
0 in INT by INT_1:def 2;
hence f . 0 = 0_No by A1, A8; :: thesis: ( f . (n + 1) = [{(f . n)},{}] & f . (- (n + 1)) = [{},{(f . (- n))}] )
A9: ( n + 1 in INT & n in INT ) by INT_1:def 2;
then ( f . (n + 1) = f1 . (n + 1) & f1 . (n + 1) = H₁(n,f1 . n) ) by A2, A8;
hence f . (n + 1) = [{(f . n)},{}] by A9, A8; :: thesis: f . (- (n + 1)) = [{},{(f . (- n))}]
A10: ( - (n + 1) in INT & - n in INT ) by INT_1:def 2;
then A11: ( f . (- (n + 1)) = f2 . (- (- (n + 1))) & f2 . (- (- (n + 1))) = H₂(n,f2 . n) ) by A4, A8;
f . (- n) = f2 . (- (- n))

proof

per cases ( n > 0 or n = 0 ) ;

suppose n > 0 ; :: thesis: f . (- n) = f2 . (- (- n))

hence f . (- n) = f2 . (- (- n)) by A10, A8; :: thesis: verum

end;

suppose n = 0 ; :: thesis: f . (- n) = f2 . (- (- n))

hence f . (- n) = f2 . (- (- n)) by A10, A1, A3, A8; :: thesis: verum

end;

end;

end;

hence f . (- (n + 1)) = [{},{(f . (- n))}] by A11; :: thesis: verum