for S1, S2 being non empty ManySortedSign st ex f, h being ManySortedSet of NAT st
( S1 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( 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) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( 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) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) holds
S1 = S2 from 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 . F5() & f . 0 = F1() & h . 0 = F2() & ( 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) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( 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) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) holds
S1 = S2 ; :: thesis: verum