for S1, S2 being non empty ManySortedSign st ex f, h being ManySortedSet of NAT st

( S1 = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( for n being Nat

for S being non empty ManySortedSign

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

( f . (n + 1) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st

( S2 = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( for n being Nat

for S being non empty ManySortedSign

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

( f . (n + 1) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) ) holds

S1 = S2 from CIRCCMB2:sch 5();

hence for S1, S2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, h being ManySortedSet of NAT st

( S1 = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( for n being Nat

for S being non empty ManySortedSign

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

( f . (n + 1) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st

( S2 = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( for n being Nat

for S being non empty ManySortedSign

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

( f . (n + 1) = F_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) ) holds

S1 = S2 ; :: thesis: verum

( S1 = f . F

for S being non empty ManySortedSign

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

( f . (n + 1) = F

( S2 = f . F

for S being non empty ManySortedSign

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

( f . (n + 1) = F

S1 = S2 from CIRCCMB2:sch 5();

hence for S1, S2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, h being ManySortedSet of NAT st

( S1 = f . F

for S being non empty ManySortedSign

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

( f . (n + 1) = F

( S2 = f . F

for S being non empty ManySortedSign

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

( f . (n + 1) = F

S1 = S2 ; :: thesis: verum