let s be SynTypes_Calculus; :: thesis: for x, y, z being type of s holds x /" (z * y) <==>. (x /" y) /" z
let x, y, z be type of s; :: thesis: x /" (z * y) <==>. (x /" y) /" z
A1: <*z*> ==>. z by Def18;
A2: <*y*> ==>. y by Def18;
A3: <*x*> ==>. x by Def18;
<*z*> ^ <*y*> ==>. z * y by A1, A2, Def18;
then <*(x /" (z * y))*> ^ (<*z*> ^ <*y*>) ==>. x by A3, Lm4;
then (<*(x /" (z * y))*> ^ <*z*>) ^ <*y*> ==>. x by FINSEQ_1:32;
then <*(x /" (z * y))*> ^ <*z*> ==>. x /" y by Def18;
then A4: <*(x /" (z * y))*> ==>. (x /" y) /" z by Def18;
<*(x /" y)*> ^ <*y*> ==>. x by A2, A3, Lm4;
then (<*((x /" y) /" z)*> ^ <*z*>) ^ <*y*> ==>. x by A1, Lm3;
then <*((x /" y) /" z)*> ^ <*(z * y)*> ==>. x by Lm9;
then <*((x /" y) /" z)*> ==>. x /" (z * y) by Def18;
hence x /" (z * y) <==>. (x /" y) /" z by A4; :: thesis: verum