let S1, S2 be non empty ManySortedSign ; :: thesis: for A1 being non-empty MSAlgebra of S1
for A2 being non-empty MSAlgebra of 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 )
let A1 be non-empty MSAlgebra of S1; :: thesis: for A2 being non-empty MSAlgebra of 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 )
let A2 be non-empty MSAlgebra of S2; :: thesis: ( the Sorts of A1 tolerates the Sorts of A2 implies 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 ) )
assume A1: the Sorts of A1 tolerates the Sorts of A2 ; :: thesis: 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 )
then A2: the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by Def4;
( dom the Sorts of A1 = the carrier of S1 & dom the Sorts of A2 = the carrier of S2 ) by PARTFUN1:def 4;
hence 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 ) by A1, A2, CARD_3:148, CARD_3:149; :: thesis: verum