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;
for A1, A2 being non-empty MSAlgebra over F₂() st 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) ) ) ) holds
A1 = A2 from CIRCCMB2:sch 18(A2);
hence for A1, A2 being strict gate`2=den Boolean Circuit of F₂() st 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) ) ) ) holds
A1 = A2 ; :: thesis: verum