A2:
for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F_{6}(S,A,x,n) is non-empty MSAlgebra over F_{5}(S,x,n)
by A1;

let A1, A2 be non-empty MSAlgebra over F_{2}(); :: thesis: ( ex f, g, h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & A1 = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{4}() & ( for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{5}(S,x,n) & g . (n + 1) = F_{6}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & A2 = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{4}() & ( for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{5}(S,x,n) & g . (n + 1) = F_{6}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) ) implies A1 = A2 )

given f1, g1, h1 being ManySortedSet of NAT such that F_{2}() = f1 . F_{8}()
and

A3: A1 = g1 . F_{8}()
and

A4: ( f1 . 0 = F_{1}() & g1 . 0 = F_{3}() )
and

A5: h1 . 0 = F_{4}()
and

A6: for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f1 . (n + 1) = F_{5}(S,x,n) & g1 . (n + 1) = F_{6}(S,A,x,n) & h1 . (n + 1) = F_{7}(x,n) )
; :: thesis: ( for f, g, h being ManySortedSet of NAT holds

( not F_{2}() = f . F_{8}() or not A2 = g . F_{8}() or not f . 0 = F_{1}() or not g . 0 = F_{3}() or not h . 0 = F_{4}() or ex n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st

( S = f . n & A = g . n & x = h . n & not ( f . (n + 1) = F_{5}(S,x,n) & g . (n + 1) = F_{6}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) ) or A1 = A2 )

A7: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = f1 . 0 & A = g1 . 0 ) by A4;

given f2, g2, h2 being ManySortedSet of NAT such that F_{2}() = f2 . F_{8}()
and

A8: A2 = g2 . F_{8}()
and

A9: ( f2 . 0 = F_{1}() & g2 . 0 = F_{3}() & h2 . 0 = F_{4}() )
and

A10: for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f2 . (n + 1) = F_{5}(S,x,n) & g2 . (n + 1) = F_{6}(S,A,x,n) & h2 . (n + 1) = F_{7}(x,n) )
; :: thesis: A1 = A2

A11: ( f1 . 0 = f2 . 0 & g1 . 0 = g2 . 0 & h1 . 0 = h2 . 0 ) by A4, A5, A9;

( f1 = f2 & g1 = g2 & h1 = h2 ) from CIRCCMB2:sch 14(A7, A11, A6, A10, A2);

hence A1 = A2 by A3, A8; :: thesis: verum

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F

let A1, A2 be non-empty MSAlgebra over F

( F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F

( F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F

given f1, g1, h1 being ManySortedSet of NAT such that F

A3: A1 = g1 . F

A4: ( f1 . 0 = F

A5: h1 . 0 = F

A6: for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f1 . (n + 1) = F

( not F

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

A7: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = f1 . 0 & A = g1 . 0 ) by A4;

given f2, g2, h2 being ManySortedSet of NAT such that F

A8: A2 = g2 . F

A9: ( f2 . 0 = F

A10: for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f2 . (n + 1) = F

A11: ( f1 . 0 = f2 . 0 & g1 . 0 = g2 . 0 & h1 . 0 = h2 . 0 ) by A4, A5, A9;

( f1 = f2 & g1 = g2 & h1 = h2 ) from CIRCCMB2:sch 14(A7, A11, A6, A10, A2);

hence A1 = A2 by A3, A8; :: thesis: verum