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