let S1, S2 be non empty ManySortedSign ; :: thesis: ( ex f, h being ManySortedSet of NAT st

( S1 = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( 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_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st

( S2 = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( 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_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) ) implies S1 = S2 )

given f1, h1 being ManySortedSet of NAT such that A1: S1 = f1 . F_{5}()
and

A2: f1 . 0 = F_{1}()
and

A3: h1 . 0 = F_{2}()
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_{3}(S,x,n) & h1 . (n + 1) = F_{4}(x,n) )
; :: thesis: ( for f, h being ManySortedSet of NAT holds

( not S2 = f . F_{5}() or not f . 0 = F_{1}() or not h . 0 = F_{2}() 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_{3}(S,x,n) & h . (n + 1) = F_{4}(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_{3}(S,x,n) & h1 . (n + 1) = F_{4}(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_{1}[S,x,n] holds

S_{1}[F_{3}(S,x,n),F_{4}(x,n),n + 1]
;

A7: ex S being non empty ManySortedSign ex x being set st

( S = f1 . 0 & x = h1 . 0 & S_{1}[S,x, 0 ] )
by A2;

A8: for n being Nat ex S being non empty ManySortedSign st

( S = f1 . n & S_{1}[S,h1 . n,n] )
from CIRCCMB2:sch 2(A7, A5, A6);

given f2, h2 being ManySortedSet of NAT such that A9: S2 = f2 . F_{5}()
and

A10: f2 . 0 = F_{1}()
and

A11: h2 . 0 = F_{2}()
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_{3}(S,x,n) & h2 . (n + 1) = F_{4}(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_{3}(S,x,n) & h2 . (n + 1) = F_{4}(x,n) )
by A12;

defpred S_{2}[ 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_{1}[S,x,n] holds

S_{1}[F_{3}(S,x,n),F_{4}(x,n),n + 1]
;

A15: ex S being non empty ManySortedSign ex x being set st

( S = f2 . 0 & x = h2 . 0 & S_{1}[S,x, 0 ] )
by A10;

A16: for n being Nat ex S being non empty ManySortedSign st

( S = f2 . n & S_{1}[S,h2 . n,n] )
from CIRCCMB2:sch 2(A15, A13, A14);

_{3}[ Nat] means f1 . $1 = f2 . $1;

A20: S_{2}[ 0 ]
by A3, A11;

for i being Nat holds S_{2}[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;

_{3}[ 0 ]
by A2, A10;

for i being Nat holds S_{3}[i]
from NAT_1:sch 2(A25, A22);

hence S1 = S2 by A1, A9; :: thesis: verum

( S1 = f . F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

( S2 = f . F

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = F

given f1, h1 being ManySortedSet of NAT such that A1: S1 = f1 . F

A2: f1 . 0 = F

A3: h1 . 0 = F

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

( not S2 = f . F

( S = f . n & x = h . n & not ( f . (n + 1) = F

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

A6: for n being Nat

for S being non empty ManySortedSign

for x being set st S = f1 . n & x = h1 . n & S

S

A7: ex S being non empty ManySortedSign ex x being set st

( S = f1 . 0 & x = h1 . 0 & S

A8: for n being Nat ex S being non empty ManySortedSign st

( S = f1 . n & S

given f2, h2 being ManySortedSet of NAT such that A9: S2 = f2 . F

A10: f2 . 0 = F

A11: h2 . 0 = F

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

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

defpred S

A14: for n being Nat

for S being non empty ManySortedSign

for x being set st S = f2 . n & x = h2 . n & S

S

A15: ex S being non empty ManySortedSign ex x being set st

( S = f2 . 0 & x = h2 . 0 & S

A16: for n being Nat ex S being non empty ManySortedSign st

( S = f2 . n & S

A17: now :: thesis: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]

defpred SS

let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume A18: S_{2}[n]
; :: thesis: S_{2}[n + 1]

ex S being non empty ManySortedSign st

( S = f1 . n & S_{1}[S,h1 . n,n] )
by A8;

then A19: h1 . (n + 1) = F_{4}((h1 . n),n)
by A4;

ex S being non empty ManySortedSign st

( S = f2 . n & S_{1}[S,h2 . n,n] )
by A16;

hence S_{2}[n + 1]
by A12, A18, A19; :: thesis: verum

end;assume A18: S

ex S being non empty ManySortedSign st

( S = f1 . n & S

then A19: h1 . (n + 1) = F

ex S being non empty ManySortedSign st

( S = f2 . n & S

hence S

A20: S

for i being Nat holds S

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_{3}[n] holds

S_{3}[n + 1]

A25:
SS

let n be Nat; :: thesis: ( S_{3}[n] implies S_{3}[n + 1] )

assume A23: S_{3}[n]
; :: thesis: S_{3}[n + 1]

consider S being non empty ManySortedSign such that

A24: S = f1 . n and

S_{1}[S,h1 . n,n]
by A8;

f1 . (n + 1) = F_{3}(S,(h1 . n),n)
by A4, A24

.= f2 . (n + 1) by A12, A21, A23, A24 ;

hence S_{3}[n + 1]
; :: thesis: verum

end;assume A23: S

consider S being non empty ManySortedSign such that

A24: S = f1 . n and

S

f1 . (n + 1) = F

.= f2 . (n + 1) by A12, A21, A23, A24 ;

hence S

for i being Nat holds S

hence S1 = S2 by A1, A9; :: thesis: verum