theorem :: CIRCCOMB:25

for S1, S2 being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S1
for s1 being Element of product the Sorts of A1
for A2 being non-empty MSAlgebra over S2
for s2 being Element of product the Sorts of A2 st the Sorts of A1 tolerates the Sorts of A2 holds
s1 +* s2 in product the Sorts of (A1 +* A2)