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