set f = the Choice_Function of Class (==_ X);
A5: union (Class (==_ X)) = the carrier' of X by EQREL_1:def 4;
then reconsider f = the Choice_Function of Class (==_ X) as Function of (Class (==_ X)), the carrier' of X ;
consider s being stack of X such that
A6: emp s by Th2;
A7: Class ((==_ X),s) = the s_empty of X by A6, Th19;
reconsider E = Class ((==_ X),s) as Element of Class (==_ X) by EQREL_1:def 3;
set g = the s_top of X * f;
take X1 = StackSystem(# the carrier of X,(Class (==_ X)),{E},( the s_push of X /\/ (==_ X)),(( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X)),(( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) #); :: thesis: ( the carrier of X1 = the carrier of X & the carrier' of X1 = Class (==_ X) & the s_empty of X1 = { the s_empty of X} & the s_push of X1 = the s_push of X /\/ (==_ X) & the s_pop of X1 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) & ( for f being Choice_Function of Class (==_ X) holds the s_top of X1 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X) ) )
thus ( the carrier of X1 = the carrier of X & the carrier' of X1 = Class (==_ X) & the s_empty of X1 = { the s_empty of X} & the s_push of X1 = the s_push of X /\/ (==_ X) & the s_pop of X1 = ( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X) ) by A6, Th19; :: thesis: for f being Choice_Function of Class (==_ X) holds the s_top of X1 = ( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)
let h be Choice_Function of Class (==_ X); :: thesis: the s_top of X1 = ( the s_top of X * h) +* ( the s_empty of X, the Element of the carrier of X)
reconsider h0 = h as Function of (Class (==_ X)), the carrier' of X by A5;

now :: thesis: for a being Element of Class (==_ X) holds (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . a = (( the s_top of X * h0) +* ( the s_empty of X, the Element of the carrier of X)) . a

let a be Element of Class (==_ X); :: thesis: (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . b₁ = (( the s_top of X * h0) +* ( the s_empty of X, the Element of the carrier of X)) . b₁
consider s1 being stack of X such that
A8: a = Class ((==_ X),s1) by EQREL_1:36;

per cases ( emp s1 or not emp s1 ) ;

suppose emp s1 ; :: thesis: (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . b₁ = (( the s_top of X * h0) +* ( the s_empty of X, the Element of the carrier of X)) . b₁

then ( s1 in the s_empty of X & dom ( the s_top of X * f) = Class (==_ X) & dom ( the s_top of X * h0) = Class (==_ X) ) by Def3, FUNCT_2:def 1;
then A9: ( a = E & E in dom ( the s_top of X * f) & E in dom ( the s_top of X * h0) ) by A7, A8, EQREL_1:23;
then (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . a = the Element of the carrier of X by A7, FUNCT_7:31;
hence (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . a = (( the s_top of X * h0) +* ( the s_empty of X, the Element of the carrier of X)) . a by A7, A9, FUNCT_7:31; :: thesis: verum

end;

suppose A10: not emp s1 ; :: thesis: (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . b₁ = (( the s_top of X * h0) +* ( the s_empty of X, the Element of the carrier of X)) . b₁

then s1 nin E by A7, Def3;
then A11: a <> E by A8, EQREL_1:23;
{} nin Class (==_ X) by SETFAM_1:def 8;
then ( f . a in a & h . a in a ) by ORDERS_1:def 1;
then ( [s1,(f . a)] in ==_ X & [s1,(h . a)] in ==_ X ) by A8, EQREL_1:18;
then ( s1 == f . a & s1 == h0 . a ) by Def16;
then ( f . a == h0 . a & not emp f . a ) by A10, Th13, Th14;
then top (f . a) = top (h0 . a) by Th18;
then ( the s_top of X * f) . a = top (h0 . a) by FUNCT_2:15;
then ( the s_top of X * f) . a = ( the s_top of X * h0) . a by FUNCT_2:15;
then (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . a = ( the s_top of X * h0) . a by A7, A11, FUNCT_7:32;
hence (( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . a = (( the s_top of X * h0) +* ( the s_empty of X, the Element of the carrier of X)) . a by A7, A11, FUNCT_7:32; :: thesis: verum

end;

end;

end;

hence the s_top of X1 = ( the s_top of X * h) +* ( the s_empty of X, the Element of the carrier of X) by FUNCT_2:63; :: thesis: verum