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