deffunc H₁( Element of X, Element of the carrier of X * ) -> Element of the carrier of X * = <*$1*> ^ $2;
reconsider w = <*> the carrier of X as Element of the carrier of X * by FINSEQ_1:def 11;
ex a being Element of the carrier of X * ex F being Function of the carrier' of X,( the carrier of X *) st
( a = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = w ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = H₁(e,F . s1) ) ) from STACKS_1:sch 4();
hence ex b₁ being Element of the carrier of X * ex F being Function of the carrier' of X,( the carrier of X *) st
( b₁ = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) ) ; :: thesis: verum