for I being set
for S being non empty non void ManySortedSign
for E being EqualSet of S
for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i & A |= E ) ) holds
product F |= E