let S1, S2 be non empty ManySortedSign ; :: thesis: ( ex f, h being ManySortedSet of NAT st
( S1 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) implies S1 = S2 )
given f1, h1 being ManySortedSet of NAT such that A1: S1 = f1 . F5() and
A2: f1 . 0 = F1() and
A3: h1 . 0 = F2() and
A4: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f1 . n & x = h1 . n holds
( f1 . (n + 1) = F3(S,x,n) & h1 . (n + 1) = F4(x,n) ) ; :: thesis: ( for f, h being ManySortedSet of NAT holds
( not S2 = f . F5() or not f . 0 = F1() or not h . 0 = F2() or ex n being Nat ex S being non empty ManySortedSign ex x being set st
( S = f . n & x = h . n & not ( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) or S1 = S2 )
A5: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f1 . n & x = h1 . n holds
( f1 . (n + 1) = F3(S,x,n) & h1 . (n + 1) = F4(x,n) ) by A4;
A6: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f1 . n & x = h1 . n & S1[S,x,n] holds
S1[F3(S,x,n),F4(x,n),n + 1] ;
A7: ex S being non empty ManySortedSign ex x being set st
( S = f1 . 0 & x = h1 . 0 & S1[S,x, 0 ] ) by A2;
A8: for n being Nat ex S being non empty ManySortedSign st
( S = f1 . n & S1[S,h1 . n,n] ) from CIRCCMB2:sch 2(A7, A5, A6);
 given f2, h2 being ManySortedSet of NAT such that A9: S2 = f2 . F5() and
A10: f2 . 0 = F1() and
A11: h2 . 0 = F2() and
A12: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f2 . n & x = h2 . n holds
( f2 . (n + 1) = F3(S,x,n) & h2 . (n + 1) = F4(x,n) ) ; :: thesis: S1 = S2
A13: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f2 . n & x = h2 . n holds
( f2 . (n + 1) = F3(S,x,n) & h2 . (n + 1) = F4(x,n) ) by A12;
defpred S2[ Nat] means h1 . $1 = h2 . $1;
A14: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f2 . n & x = h2 . n & S1[S,x,n] holds
S1[F3(S,x,n),F4(x,n),n + 1] ;
A15: ex S being non empty ManySortedSign ex x being set st
( S = f2 . 0 & x = h2 . 0 & S1[S,x, 0 ] ) by A10;
A16: for n being Nat ex S being non empty ManySortedSign st
( S = f2 . n & S1[S,h2 . n,n] ) from CIRCCMB2:sch 2(A15, A13, A14);
A17: now :: thesis: for n being Nat st S2[n] holds
S2[n + 1]
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A18: S2[n] ; :: thesis: S2[n + 1]
ex S being non empty ManySortedSign st
( S = f1 . n & S1[S,h1 . n,n] ) by A8;
then A19: h1 . (n + 1) = F4((h1 . n),n) by A4;
ex S being non empty ManySortedSign st
( S = f2 . n & S1[S,h2 . n,n] ) by A16;
hence S2[n + 1] by A12, A18, A19; :: thesis: verum
end;
defpred S3[ Nat] means f1 . $1 = f2 . $1;
A20: S2[ 0 ] by A3, A11;
for i being Nat holds S2[i] from NAT_1:sch 2(A20, A17);
 then for i being object st i in NAT holds
h1 . i = h2 . i ;
then A21: h1 = h2 by PBOOLE:3;
A22: now :: thesis: for n being Nat st S3[n] holds
S3[n + 1]
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
assume A23: S3[n] ; :: thesis: S3[n + 1]
consider S being non empty ManySortedSign such that
A24: S = f1 . n and
S1[S,h1 . n,n] by A8;
f1 . (n + 1) = F3(S,(h1 . n),n) by A4, A24
.= f2 . (n + 1) by A12, A21, A23, A24 ;
hence S3[n + 1] ; :: thesis: verum
end;
A25: S3[ 0 ] by A2, A10;
for i being Nat holds S3[i] from NAT_1:sch 2(A25, A22);
 hence S1 = S2 by A1, A9; :: thesis: verum