let s be SynTypes_Calculus; :: thesis: for T being FinSequence of s
for x, y, z being type of s st T ==>. y & <*x*> ==>. z holds
T ^ <*(y \ x)*> ==>. z
let T be FinSequence of s; :: thesis: for x, y, z being type of s st T ==>. y & <*x*> ==>. z holds
T ^ <*(y \ x)*> ==>. z
let x, y, z be type of s; :: thesis: ( T ==>. y & <*x*> ==>. z implies T ^ <*(y \ x)*> ==>. z )
assume that
A1: T ==>. y and
A2: <*x*> ==>. z ; :: thesis: T ^ <*(y \ x)*> ==>. z
H₂(s) ^ <*x*> ==>. z by A2, FINSEQ_1:34;
then (H₂(s) ^ T) ^ <*(y \ x)*> ==>. z by A1, Lm5;
hence T ^ <*(y \ x)*> ==>. z by FINSEQ_1:34; :: thesis: verum