for n being Nat
for I being set st n >= 4 holds
for B being non empty non void bool-correct BoolSignature st B is n,I integer holds
for A1 being non-empty bool-correct MSAlgebra over B st A1 is n,I integer holds
for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
for A2 being non-empty MSAlgebra over C st the Sorts of A1 tolerates the Sorts of A2 holds
for S being non empty non void bool-correct BoolSignature st BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C holds
for A being non-empty bool-correct MSAlgebra over S st A = (B,A1) +* A2 holds
A is n,I integer