scheme :: CIRCCMB2:sch 16
CIRCCMB29sch16{ F₁() -> non empty ManySortedSign , F₂() -> non-empty MSAlgebra over F₁(), F₃() -> object , F₄( object , object , object ) -> non empty ManySortedSign , F₅( object , object , object , object ) -> object , F₆( object , object ) -> object , F₇() -> Nat } :

ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex f, g, h being ManySortedSet of NAT st
( S = f . F₇() & A = g . F₇() & f . 0 = F₁() & g . 0 = F₂() & h . 0 = F₃() & ( 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₄(S,x,n) & g . (n + 1) = F₅(S,A,x,n) & h . (n + 1) = F₆(x,n) ) ) )

provided

A1: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F₅(S,A,x,n) is non-empty MSAlgebra over F₄(S,x,n)