for I being set
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of (Equations S) . 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