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;

for A1, A2 being non-empty MSAlgebra over F_{2}() st 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) ) ) ) holds

A1 = A2 from CIRCCMB2:sch 18(A2);

hence for A1, A2 being strict gate`2=den Boolean Circuit of F_{2}() st 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) ) ) ) holds

A1 = A2 ; :: thesis: verum

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F

for A1, A2 being 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

A1 = A2 from CIRCCMB2:sch 18(A2);

hence for A1, A2 being strict gate`2=den Boolean Circuit of 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

A1 = A2 ; :: thesis: verum