let s be SynTypes_Calculus; :: thesis: for x, y, z being type of s holds (x * y) * z <==>. x * (y * z)
let x, y, z be type of s; :: thesis: (x * y) * z <==>. x * (y * z)
A1: <*x*> ==>. x by Def19;
A2: <*y*> ==>. y by Def19;
A3: <*z*> ==>. z by Def19;
<*x*> ^ <*y*> ==>. x * y by A1, A2, Def19;
then (<*x*> ^ <*y*>) ^ <*z*> ==>. (x * y) * z by A3, Def19;
then <*x*> ^ <*(y * z)*> ==>. (x * y) * z by Lm11;
then A4: <*(x * (y * z))*> ==>. (x * y) * z by Lm12;
<*y*> ^ <*z*> ==>. y * z by A2, A3, Def19;
then <*x*> ^ (<*y*> ^ <*z*>) ==>. x * (y * z) by A1, Def19;
then (<*x*> ^ <*y*>) ^ <*z*> ==>. x * (y * z) by FINSEQ_1:45;
then <*(x * y)*> ^ <*z*> ==>. x * (y * z) by Lm10;
then <*((x * y) * z)*> ==>. x * (y * z) by Lm12;
hence (x * y) * z <==>. x * (y * z) by A4, Def20; :: thesis: verum