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