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