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₆(S,A,x,n) is non-empty MSAlgebra over F₅(S,x,n) by A1;
let A1, A2 be non-empty MSAlgebra over F₂(); :: thesis: ( ex f, g, h being ManySortedSet of NAT st
( F₂() = f . F₈() & A1 = g . F₈() & f . 0 = F₁() & g . 0 = F₃() & h . 0 = F₄() & ( 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₅(S,x,n) & g . (n + 1) = F₆(S,A,x,n) & h . (n + 1) = F₇(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( F₂() = f . F₈() & A2 = g . F₈() & f . 0 = F₁() & g . 0 = F₃() & h . 0 = F₄() & ( 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₅(S,x,n) & g . (n + 1) = F₆(S,A,x,n) & h . (n + 1) = F₇(x,n) ) ) ) implies A1 = A2 )
given f1, g1, h1 being ManySortedSet of NAT such that F₂() = f1 . F₈() and
A3: A1 = g1 . F₈() and
A4: ( f1 . 0 = F₁() & g1 . 0 = F₃() ) and
A5: h1 . 0 = F₄() 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₅(S,x,n) & g1 . (n + 1) = F₆(S,A,x,n) & h1 . (n + 1) = F₇(x,n) ) ; :: thesis: ( for f, g, h being ManySortedSet of NAT holds
( not F₂() = f . F₈() or not A2 = g . F₈() or not f . 0 = F₁() or not g . 0 = F₃() or not h . 0 = F₄() 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₅(S,x,n) & g . (n + 1) = F₆(S,A,x,n) & h . (n + 1) = F₇(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₂() = f2 . F₈() and
A8: A2 = g2 . F₈() and
A9: ( f2 . 0 = F₁() & g2 . 0 = F₃() & h2 . 0 = F₄() ) 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₅(S,x,n) & g2 . (n + 1) = F₆(S,A,x,n) & h2 . (n + 1) = F₇(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