theorem :: CIRCCOMB:26

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