let S1, S2 be non empty ManySortedSign ; :: thesis: ( ex f, h being ManySortedSet of NAT st
( S1 = f . F₅() & f . 0 = F₁() & h . 0 = F₂() & ( 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) = F₃(S,x,n) & h . (n + 1) = F₄(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F₅() & f . 0 = F₁() & h . 0 = F₂() & ( 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) = F₃(S,x,n) & h . (n + 1) = F₄(x,n) ) ) ) implies S1 = S2 )
given f1, h1 being ManySortedSet of NAT such that A1: S1 = f1 . F₅() and
A2: f1 . 0 = F₁() and
A3: h1 . 0 = F₂() 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) = F₃(S,x,n) & h1 . (n + 1) = F₄(x,n) ) ; :: thesis: ( for f, h being ManySortedSet of NAT holds
( not S2 = f . F₅() or not f . 0 = F₁() or not h . 0 = F₂() 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) = F₃(S,x,n) & h . (n + 1) = F₄(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) = F₃(S,x,n) & h1 . (n + 1) = F₄(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 & S₁[S,x,n] holds
S₁[F₃(S,x,n),F₄(x,n),n + 1] ;
A7: ex S being non empty ManySortedSign ex x being set st
( S = f1 . 0 & x = h1 . 0 & S₁[S,x, 0 ] ) by A2;
A8: for n being Nat ex S being non empty ManySortedSign st
( S = f1 . n & S₁[S,h1 . n,n] ) from CIRCCMB2:sch 2(A7, A5, A6);
given f2, h2 being ManySortedSet of NAT such that A9: S2 = f2 . F₅() and
A10: f2 . 0 = F₁() and
A11: h2 . 0 = F₂() 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) = F₃(S,x,n) & h2 . (n + 1) = F₄(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) = F₃(S,x,n) & h2 . (n + 1) = F₄(x,n) ) by A12;
defpred S₂[ 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 & S₁[S,x,n] holds
S₁[F₃(S,x,n),F₄(x,n),n + 1] ;
A15: ex S being non empty ManySortedSign ex x being set st
( S = f2 . 0 & x = h2 . 0 & S₁[S,x, 0 ] ) by A10;
A16: for n being Nat ex S being non empty ManySortedSign st
( S = f2 . n & S₁[S,h2 . n,n] ) from CIRCCMB2:sch 2(A15, A13, A14);

A17: now :: thesis: for n being Nat st S₂[n] holds
S₂[n + 1]

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A18: S₂[n] ; :: thesis: S₂[n + 1]
ex S being non empty ManySortedSign st
( S = f1 . n & S₁[S,h1 . n,n] ) by A8;
then A19: h1 . (n + 1) = F₄((h1 . n),n) by A4;
ex S being non empty ManySortedSign st
( S = f2 . n & S₁[S,h2 . n,n] ) by A16;
hence S₂[n + 1] by A12, A18, A19; :: thesis: verum

end;

defpred S₃[ Nat] means f1 . $1 = f2 . $1;
A20: S₂[ 0 ] by A3, A11;
for i being Nat holds S₂[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 S₃[n] holds
S₃[n + 1]

let n be Nat; :: thesis: ( S₃[n] implies S₃[n + 1] )
assume A23: S₃[n] ; :: thesis: S₃[n + 1]
consider S being non empty ManySortedSign such that
A24: S = f1 . n and
S₁[S,h1 . n,n] by A8;
f1 . (n + 1) = F₃(S,(h1 . n),n) by A4, A24
.= f2 . (n + 1) by A12, A21, A23, A24 ;
hence S₃[n + 1] ; :: thesis: verum

end;

A25: S₃[ 0 ] by A2, A10;
for i being Nat holds S₃[i] from NAT_1:sch 2(A25, A22);
hence S1 = S2 by A1, A9; :: thesis: verum