let S1, S2, S3 be non empty ManySortedSign ; :: thesis: for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over S2
for A3 being non-empty MSAlgebra over S3 st the Sorts of A1 tolerates the Sorts of A2 & the Sorts of A2 tolerates the Sorts of A3 & the Sorts of A3 tolerates the Sorts of A1 holds
(A1 +* A2) +* A3 = A1 +* (A2 +* A3)
let A1 be non-empty MSAlgebra over S1; :: thesis: for A2 being non-empty MSAlgebra over S2
for A3 being non-empty MSAlgebra over S3 st the Sorts of A1 tolerates the Sorts of A2 & the Sorts of A2 tolerates the Sorts of A3 & the Sorts of A3 tolerates the Sorts of A1 holds
(A1 +* A2) +* A3 = A1 +* (A2 +* A3)
let A2 be non-empty MSAlgebra over S2; :: thesis: for A3 being non-empty MSAlgebra over S3 st the Sorts of A1 tolerates the Sorts of A2 & the Sorts of A2 tolerates the Sorts of A3 & the Sorts of A3 tolerates the Sorts of A1 holds
(A1 +* A2) +* A3 = A1 +* (A2 +* A3)
let A3 be non-empty MSAlgebra over S3; :: thesis: ( the Sorts of A1 tolerates the Sorts of A2 & the Sorts of A2 tolerates the Sorts of A3 & the Sorts of A3 tolerates the Sorts of A1 implies (A1 +* A2) +* A3 = A1 +* (A2 +* A3) )
assume that
A1: the Sorts of A1 tolerates the Sorts of A2 and
A2: the Sorts of A2 tolerates the Sorts of A3 and
A3: the Sorts of A3 tolerates the Sorts of A1 ; :: thesis: (A1 +* A2) +* A3 = A1 +* (A2 +* A3)
set A12 = A1 +* A2;
set A23 = A2 +* A3;
A4: the Charact of (A1 +* A2) = the Charact of A1 +* the Charact of A2 by A1, Def4;
set A1293 = (A1 +* A2) +* A3;
set A1923 = A1 +* (A2 +* A3);
set s1 = the Sorts of A1;
set s2 = the Sorts of A2;
set s3 = the Sorts of A3;
A5: the Sorts of (A2 +* A3) = the Sorts of A2 +* the Sorts of A3 by A2, Def4;
A6: the Sorts of A1 tolerates the Sorts of (A2 +* A3)

proof

let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (proj1 the Sorts of A1) /\ (proj1 the Sorts of (A2 +* A3)) or the Sorts of A1 . x = the Sorts of (A2 +* A3) . x )
assume A7: x in (dom the Sorts of A1) /\ (dom the Sorts of (A2 +* A3)) ; :: thesis: the Sorts of A1 . x = the Sorts of (A2 +* A3) . x
then x in dom the Sorts of (A2 +* A3) by XBOOLE_0:def 4;
then A8: ( x in dom the Sorts of A2 or x in dom the Sorts of A3 ) by A5, FUNCT_4:12;
x in dom the Sorts of A1 by A7, XBOOLE_0:def 4;
then ( ( x in (dom the Sorts of A1) /\ (dom the Sorts of A2) & ( the Sorts of A2 +* the Sorts of A3) . x = the Sorts of A2 . x ) or ( x in (dom the Sorts of A3) /\ (dom the Sorts of A1) & ( the Sorts of A2 +* the Sorts of A3) . x = the Sorts of A3 . x ) ) by A2, A8, FUNCT_4:13, FUNCT_4:15, XBOOLE_0:def 4;
hence the Sorts of A1 . x = the Sorts of (A2 +* A3) . x by A1, A3, A5; :: thesis: verum

end;

then A9: the Sorts of (A1 +* (A2 +* A3)) = the Sorts of A1 +* the Sorts of (A2 +* A3) by Def4;
A10: the Charact of (A2 +* A3) = the Charact of A2 +* the Charact of A3 by A2, Def4;
A11: the Charact of (A1 +* (A2 +* A3)) = the Charact of A1 +* the Charact of (A2 +* A3) by A6, Def4;
A12: the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by A1, Def4;
A13: the Sorts of (A1 +* A2) tolerates the Sorts of A3

proof

let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (proj1 the Sorts of (A1 +* A2)) /\ (proj1 the Sorts of A3) or the Sorts of (A1 +* A2) . x = the Sorts of A3 . x )
assume A14: x in (dom the Sorts of (A1 +* A2)) /\ (dom the Sorts of A3) ; :: thesis: the Sorts of (A1 +* A2) . x = the Sorts of A3 . x
then x in dom the Sorts of (A1 +* A2) by XBOOLE_0:def 4;
then A15: ( x in dom the Sorts of A1 or x in dom the Sorts of A2 ) by A12, FUNCT_4:12;
x in dom the Sorts of A3 by A14, XBOOLE_0:def 4;
then ( ( x in (dom the Sorts of A3) /\ (dom the Sorts of A1) & ( the Sorts of A1 +* the Sorts of A2) . x = the Sorts of A1 . x ) or ( x in (dom the Sorts of A2) /\ (dom the Sorts of A3) & ( the Sorts of A1 +* the Sorts of A2) . x = the Sorts of A2 . x ) ) by A1, A15, FUNCT_4:13, FUNCT_4:15, XBOOLE_0:def 4;
hence the Sorts of (A1 +* A2) . x = the Sorts of A3 . x by A2, A3, A12; :: thesis: verum

end;

then the Charact of ((A1 +* A2) +* A3) = the Charact of (A1 +* A2) +* the Charact of A3 by Def4;
then A16: the Charact of ((A1 +* A2) +* A3) = the Charact of (A1 +* (A2 +* A3)) by A4, A10, A11, FUNCT_4:14;
the Sorts of ((A1 +* A2) +* A3) = the Sorts of (A1 +* A2) +* the Sorts of A3 by A13, Def4;
then the Sorts of ((A1 +* A2) +* A3) = the Sorts of (A1 +* (A2 +* A3)) by A12, A5, A9, FUNCT_4:14;
hence (A1 +* A2) +* A3 = A1 +* (A2 +* A3) by A16; :: thesis: verum