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