let S1, S2 be non empty ManySortedSign ; :: thesis: ( S1 tolerates S2 implies S1 +* S2 = S2 +* S1 )
set S = S1 +* S2;
assume ( the Arity of S1 tolerates the Arity of S2 & the ResultSort of S1 tolerates the ResultSort of S2 ) ; :: according to CIRCCOMB:def 1 :: thesis: S1 +* S2 = S2 +* S1
then ( the Arity of S1 +* the Arity of S2 = the Arity of S2 +* the Arity of S1 & the ResultSort of S1 +* the ResultSort of S2 = the ResultSort of S2 +* the ResultSort of S1 ) by FUNCT_4:35;
then ( the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 & the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 & the Arity of (S1 +* S2) = the Arity of S2 +* the Arity of S1 & the ResultSort of (S1 +* S2) = the ResultSort of S2 +* the ResultSort of S1 ) by Def2;
hence S1 +* S2 = S2 +* S1 by Def2; :: thesis: verum