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 & <*y*> ==>. y & <*z*> ==>. z ) by Def19;
then ( <*x*> ^ <*y*> ==>. x * y & <*z*> ==>. z ) by Def19;
then (<*x*> ^ <*y*>) ^ <*z*> ==>. (x * y) * z by Def19;
then <*x*> ^ <*(y * z)*> ==>. (x * y) * z by Lm13;
then A2: <*(x * (y * z))*> ==>. (x * y) * z by Lm14;
( <*x*> ==>. x & <*y*> ^ <*z*> ==>. y * z ) by A1, Def19;
then <*x*> ^ (<*y*> ^ <*z*>) ==>. x * (y * z) by Def19;
then (<*x*> ^ <*y*>) ^ <*z*> ==>. x * (y * z) by FINSEQ_1:45;
then <*(x * y)*> ^ <*z*> ==>. x * (y * z) by Lm12;
then <*((x * y) * z)*> ==>. x * (y * z) by Lm14;
hence (x * y) * z <==>. x * (y * z) by A2, Def20; :: thesis: verum