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
( <*x*> ==>. x & <*y*> ==>. y & <*z*> ==>. z ) by Def19;
then ( <*x*> ^ <*y*> ==>. x * y & <*z*> ==>. z ) by Def19;
then (<*x*> ^ <*(y /" z)*>) ^ <*z*> ==>. x * y by Lm6;
then <*(x * (y /" z))*> ^ <*z*> ==>. x * y by Lm12;
hence <*(x * (y /" z))*> ==>. (x * y) /" z by Def19; :: thesis: verum