let S1, S2, S3 be non empty ManySortedSign ; :: thesis: (S1 +* S2) +* S3 = S1 +* (S2 +* S3)
set S12 = S1 +* S2;
set S23 = S2 +* S3;
set S12'3 = (S1 +* S2) +* S3;
set S1'23 = S1 +* (S2 +* S3);
A1: ( 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 S1 +* the Arity of S2 & the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 ) by Def2;
A2: ( the carrier of (S2 +* S3) = the carrier of S2 \/ the carrier of S3 & the carrier' of (S2 +* S3) = the carrier' of S2 \/ the carrier' of S3 & the Arity of (S2 +* S3) = the Arity of S2 +* the Arity of S3 & the ResultSort of (S2 +* S3) = the ResultSort of S2 +* the ResultSort of S3 ) by Def2;
A3: ( the carrier of ((S1 +* S2) +* S3) = the carrier of (S1 +* S2) \/ the carrier of S3 & the carrier' of ((S1 +* S2) +* S3) = the carrier' of (S1 +* S2) \/ the carrier' of S3 & the Arity of ((S1 +* S2) +* S3) = the Arity of (S1 +* S2) +* the Arity of S3 & the ResultSort of ((S1 +* S2) +* S3) = the ResultSort of (S1 +* S2) +* the ResultSort of S3 ) by Def2;
( the carrier of (S1 +* (S2 +* S3)) = the carrier of S1 \/ the carrier of (S2 +* S3) & the carrier' of (S1 +* (S2 +* S3)) = the carrier' of S1 \/ the carrier' of (S2 +* S3) & the Arity of (S1 +* (S2 +* S3)) = the Arity of S1 +* the Arity of (S2 +* S3) & the ResultSort of (S1 +* (S2 +* S3)) = the ResultSort of S1 +* the ResultSort of (S2 +* S3) ) by Def2;
then ( the carrier of ((S1 +* S2) +* S3) = the carrier of (S1 +* (S2 +* S3)) & the carrier' of ((S1 +* S2) +* S3) = the carrier' of (S1 +* (S2 +* S3)) & the Arity of ((S1 +* S2) +* S3) = the Arity of (S1 +* (S2 +* S3)) & the ResultSort of ((S1 +* S2) +* S3) = the ResultSort of (S1 +* (S2 +* S3)) ) by A1, A2, A3, FUNCT_4:15, XBOOLE_1:4;
hence (S1 +* S2) +* S3 = S1 +* (S2 +* S3) ; :: thesis: verum