A2: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F6(S,A,x,n) is non-empty MSAlgebra over F5(S,x,n) by A1;
for A1, A2 being non-empty MSAlgebra over F2() st ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A1 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A2 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) holds
A1 = A2 from hence for A1, A2 being strict gate`2=den Boolean Circuit of F2() st ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A1 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A2 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) holds
A1 = A2 ; :: thesis: verum