let s be SynTypes_Calculus; :: thesis: for x, y, z being type of s holds <*(x /" y)*> ==>. (x /" z) /" (y /" z)
let x, y, z be type of s; :: thesis: <*(x /" y)*> ==>. (x /" z) /" (y /" z)
A1: <*(x /" y)*> ^ <*y*> ==>. x by Th12;
<*z*> ==>. z by Def18;
then (<*(x /" y)*> ^ <*(y /" z)*>) ^ <*z*> ==>. x by A1, Lm2;
then <*(x /" y)*> ^ <*(y /" z)*> ==>. x /" z by Def18;
hence <*(x /" y)*> ==>. (x /" z) /" (y /" z) by Def18; :: thesis: verum