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;
for a1, a2 being Element of the carrier of X * st ex F being Function of the carrier' of X,( the carrier of X *) st
( a1 = 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) ) ) & ex F being Function of the carrier' of X,( the carrier of X *) st
( a2 = 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) ) ) holds
a1 = a2 from STACKS_1:sch 5();
hence for b₁, b₂ being Element of the carrier of X * st 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) ) ) & 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) ) ) holds
b₁ = b₂ ; :: thesis: verum