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 Def18;
A2: <*y*> ==>. y by Def18;
A3: <*z*> ==>. z by Def18;
<*x*> ^ <*y*> ==>. x * y by A1, A2, Def18;
then (<*x*> ^ <*y*>) ^ <*z*> ==>. (x * y) * z by A3, Def18;
then <*x*> ^ <*(y * z)*> ==>. (x * y) * z by Lm9;
then A4: <*(x * (y * z))*> ==>. (x * y) * z by Lm10;
<*y*> ^ <*z*> ==>. y * z by A2, A3, Def18;
then <*x*> ^ (<*y*> ^ <*z*>) ==>. x * (y * z) by A1, Def18;
then (<*x*> ^ <*y*>) ^ <*z*> ==>. x * (y * z) by FINSEQ_1:32;
then <*(x * y)*> ^ <*z*> ==>. x * (y * z) by Lm8;
then <*((x * y) * z)*> ==>. x * (y * z) by Lm10;
hence (x * y) * z <==>. x * (y * z) by A4; :: thesis: verum