let it1, it2 be ManySortedSet of INT ; :: thesis: ( ( for n being Nat holds
( it1 . 0 = 0_No & it1 . (n + 1) = [{(it1 . n)},{}] & it1 . (- (n + 1)) = [{},{(it1 . (- n))}] ) ) & ( for n being Nat holds
( it2 . 0 = 0_No & it2 . (n + 1) = [{(it2 . n)},{}] & it2 . (- (n + 1)) = [{},{(it2 . (- n))}] ) ) implies it1 = it2 )
assume that
A12: for n being Nat holds
( it1 . 0 = 0_No & it1 . (n + 1) = [{(it1 . n)},{}] & it1 . (- (n + 1)) = [{},{(it1 . (- n))}] ) and
A13: for n being Nat holds
( it2 . 0 = 0_No & it2 . (n + 1) = [{(it2 . n)},{}] & it2 . (- (n + 1)) = [{},{(it2 . (- n))}] ) ; :: thesis: it1 = it2
defpred S₁[ Nat] means ( it1 . $1 = it2 . $1 & it1 . (- $1) = it2 . (- $1) );
A14: S₁[ 0 ] by A12, A13;
A15: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A16: S₁[n] ; :: thesis: S₁[n + 1]
thus it1 . (n + 1) = [{(it1 . n)},{}] by A12
.= it2 . (n + 1) by A16, A13 ; :: thesis: it1 . (- (n + 1)) = it2 . (- (n + 1))
thus it1 . (- (n + 1)) = [{},{(it1 . (- n))}] by A12
.= it2 . (- (n + 1)) by A16, A13 ; :: thesis: verum

end;

A17: for n being Nat holds S₁[n] from NAT_1:sch 2(A14, A15);
A18: ( dom it1 = INT & INT = dom it2 ) by PARTFUN1:def 2;
for o being object st o in INT holds
it1 . o = it2 . o

proof

let o be object ; :: thesis: ( o in INT implies it1 . o = it2 . o )
assume o in INT ; :: thesis: it1 . o = it2 . o
then ex n being Nat st
( o = n or o = - n ) by INT_1:2;
hence it1 . o = it2 . o by A17; :: thesis: verum

end;

hence it1 = it2 by A18, FUNCT_1:2; :: thesis: verum