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;
<*y*> ==>. y by Def18;
then A2: <*x*> ^ <*y*> ==>. x * y by A1, Def18;
<*z*> ==>. z by Def18;
then (<*x*> ^ <*(y /" z)*>) ^ <*z*> ==>. x * y by A2, Lm2;
then <*(x * (y /" z))*> ^ <*z*> ==>. x * y by Lm8;
hence <*(x * (y /" z))*> ==>. (x * y) /" z by Def18; :: thesis: verum