let s be SynTypes_Calculus; :: thesis: for T, X being FinSequence of the carrier of s
for y, x, z being type of s st T ==>. y & X ^ <*x*> ==>. z holds
(X ^ <*(x /" y)*>) ^ T ==>. z
let T, X be FinSequence of the carrier of s; :: thesis: for y, x, z being type of s st T ==>. y & X ^ <*x*> ==>. z holds
(X ^ <*(x /" y)*>) ^ T ==>. z
let y, x, z be type of s; :: thesis: ( T ==>. y & X ^ <*x*> ==>. z implies (X ^ <*(x /" y)*>) ^ T ==>. z )
assume ( T ==>. y & X ^ <*x*> ==>. z ) ; :: thesis: (X ^ <*(x /" y)*>) ^ T ==>. z
then ( T ==>. y & (X ^ <*x*>) ^ H₂(s) ==>. z ) by FINSEQ_1:47;
then ((X ^ <*(x /" y)*>) ^ T) ^ H₂(s) ==>. z by Def19;
hence (X ^ <*(x /" y)*>) ^ T ==>. z by FINSEQ_1:47; :: thesis: verum