let S1, S2, S3 be non empty ManySortedSign ; (S1 +* S2) +* S3 = S1 +* (S2 +* S3)
set S12 = S1 +* S2;
set S23 = S2 +* S3;
set S1293 = (S1 +* S2) +* S3;
set S1923 = S1 +* (S2 +* S3);
A1:
the carrier of (S2 +* S3) = the carrier of S2 \/ the carrier of S3
by Def2;
A2:
the carrier of ((S1 +* S2) +* S3) = the carrier of (S1 +* S2) \/ the carrier of S3
by Def2;
A3:
the carrier of (S1 +* (S2 +* S3)) = the carrier of S1 \/ the carrier of (S2 +* S3)
by Def2;
the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2
by Def2;
then A4:
the carrier of ((S1 +* S2) +* S3) = the carrier of (S1 +* (S2 +* S3))
by A1, A2, A3, XBOOLE_1:4;
A5:
the carrier' of (S2 +* S3) = the carrier' of S2 \/ the carrier' of S3
by Def2;
A6:
the carrier' of ((S1 +* S2) +* S3) = the carrier' of (S1 +* S2) \/ the carrier' of S3
by Def2;
A7:
the Arity of (S2 +* S3) = the Arity of S2 +* the Arity of S3
by Def2;
A8:
the Arity of (S1 +* (S2 +* S3)) = the Arity of S1 +* the Arity of (S2 +* S3)
by Def2;
A9:
the carrier' of (S1 +* (S2 +* S3)) = the carrier' of S1 \/ the carrier' of (S2 +* S3)
by Def2;
the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2
by Def2;
then A10:
the carrier' of ((S1 +* S2) +* S3) = the carrier' of (S1 +* (S2 +* S3))
by A5, A6, A9, XBOOLE_1:4;
A11:
the ResultSort of (S1 +* (S2 +* S3)) = the ResultSort of S1 +* the ResultSort of (S2 +* S3)
by Def2;
A12:
the ResultSort of ((S1 +* S2) +* S3) = the ResultSort of (S1 +* S2) +* the ResultSort of S3
by Def2;
A13:
the Arity of ((S1 +* S2) +* S3) = the Arity of (S1 +* S2) +* the Arity of S3
by Def2;
the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2
by Def2;
then A14:
the Arity of ((S1 +* S2) +* S3) = the Arity of (S1 +* (S2 +* S3))
by A7, A13, A8, FUNCT_4:14;
A15:
the ResultSort of (S2 +* S3) = the ResultSort of S2 +* the ResultSort of S3
by Def2;
the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2
by Def2;
hence
(S1 +* S2) +* S3 = S1 +* (S2 +* S3)
by A15, A12, A11, A4, A10, A14, FUNCT_4:14; verum