thus
ex S being non empty ManySortedSign ex f, h being ManySortedSet of NAT st

( S = 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) ) ) )
from CIRCCMB2:sch 4(); :: thesis: 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

thus 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(); :: thesis: verum

( S = 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 = 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

thus for S1, S2 being non empty 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 from CIRCCMB2:sch 5(); :: thesis: verum