let s be SynTypes_Calculus; :: thesis: for x, z, y being type of s holds x /" (z * y) <==>. (x /" y) /" z
let x, z, y be type of s; :: thesis: x /" (z * y) <==>. (x /" y) /" z
A1: ( <*z*> ==>. z & <*y*> ==>. y & <*x*> ==>. x ) by Def19;
then ( <*z*> ^ <*y*> ==>. z * y & <*x*> ==>. x ) by Def19;
then <*(x /" (z * y))*> ^ (<*z*> ^ <*y*>) ==>. x by Lm8;
then (<*(x /" (z * y))*> ^ <*z*>) ^ <*y*> ==>. x by FINSEQ_1:45;
then <*(x /" (z * y))*> ^ <*z*> ==>. x /" y by Def19;
then A2: <*(x /" (z * y))*> ==>. (x /" y) /" z by Def19;
( <*z*> ==>. z & <*(x /" y)*> ^ <*y*> ==>. x ) by A1, Lm8;
then (<*((x /" y) /" z)*> ^ <*z*>) ^ <*y*> ==>. x by Lm7;
then <*((x /" y) /" z)*> ^ <*(z * y)*> ==>. x by Lm13;
then <*((x /" y) /" z)*> ==>. x /" (z * y) by Def19;
hence x /" (z * y) <==>. (x /" y) /" z by A2, Def20; :: thesis: verum