for I, N being set
for S being non empty non void 1,b₁,b₂ -array ConnectivesSignature
for Y being non empty set
for X being V2() ManySortedSet of Y st ( the ResultSort of S . ( the connectives of S . 2) nin Y or X . ( the ResultSort of S . ( the connectives of S . 2)) = (X . I) ^omega ) & X . N = INT & I in Y holds
ex A being strict non-empty MSAlgebra over S st
( A is 1,I,N -array & the Sorts of A tolerates X )