let S1, S2 be non empty ManySortedSign ; :: thesis: 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 )
let A1 be non-empty MSAlgebra over S1; :: thesis: 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 )
let A2 be non-empty MSAlgebra over 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 ) )
A1: dom the Sorts of A1 = the carrier of S1 by PARTFUN1:def 2;
A2: dom the Sorts of A2 = the carrier of S2 by PARTFUN1:def 2;
assume A3: 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 the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by Def4;
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 A3, A1, A2, CARD_3:98, CARD_3:99; :: thesis: verum