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