let s be SynTypes_Calculus; :: thesis: for x, y, z being type of s st <*x*> ^ <*y*> ==>. z holds
<*(x * y)*> ==>. z
let x, y, z be type of s; :: thesis: ( <*x*> ^ <*y*> ==>. z implies <*(x * y)*> ==>. z )
assume <*x*> ^ <*y*> ==>. z ; :: thesis: <*(x * y)*> ==>. z
then (H₂(s) ^ <*x*>) ^ <*y*> ==>. z by FINSEQ_1:34;
then H₂(s) ^ <*(x * y)*> ==>. z by Lm9;
hence <*(x * y)*> ==>. z by FINSEQ_1:34; :: thesis: verum