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 A1 tolerates A2 holds
A1 +* A2 = A2 +* A1
let A1 be non-empty MSAlgebra of S1; :: thesis: for A2 being non-empty MSAlgebra of S2 st A1 tolerates A2 holds
A1 +* A2 = A2 +* A1
let A2 be non-empty MSAlgebra of S2; :: thesis: ( A1 tolerates A2 implies A1 +* A2 = A2 +* A1 )
set A = A1 +* A2;
assume A1: ( S1 tolerates S2 & the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 ) ; :: according to CIRCCOMB:def 3 :: thesis: A1 +* A2 = A2 +* A1
then ( the Sorts of A1 +* the Sorts of A2 = the Sorts of A2 +* the Sorts of A1 & the Charact of A1 +* the Charact of A2 = the Charact of A2 +* the Charact of A1 ) by FUNCT_4:35;
then ( S1 +* S2 = S2 +* S1 & the Sorts of A2 tolerates the Sorts of A1 & the Sorts of (A1 +* A2) = the Sorts of A2 +* the Sorts of A1 & the Charact of (A1 +* A2) = the Charact of A2 +* the Charact of A1 ) by A1, Def4, Th9;
hence A1 +* A2 = A2 +* A1 by Def4; :: thesis: verum