set f = the Choice_Function of (Class (==_ X));
not {} in Class (==_ X) ;
then A5: the Choice_Function of (Class (==_ X)) is Function of (Class (==_ X)),(union (Class (==_ X))) by ORDERS_1:90;
A6: 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 by A5;
consider s being stack of X such that
A7: emp s by Th2;
A8: Class ((==_ X),s) = the s_empty of X by A7, 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 A7, 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)
not {} in Class (==_ X) ;
then h is Function of (Class (==_ X)),(union (Class (==_ X))) by ORDERS_1:90;
then reconsider h0 = h as Function of (Class (==_ X)), the carrier' of X by A6;

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
A9: 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 FUNCT_2:def 1;
then A10: ( a = E & E in dom ( the s_top of X * f) & E in dom ( the s_top of X * h0) ) by A8, A9, 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 A8, 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 A8, A10, FUNCT_7:31; :: thesis: verum

end;

suppose A11: 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 A8;
then A12: a <> E by A9, EQREL_1:23;
{} nin Class (==_ X) ;
then ( f . a in a & h . a in a ) by ORDERS_1:89;
then ( [s1,(f . a)] in ==_ X & [s1,(h . a)] in ==_ X ) by A9, EQREL_1:18;
then ( s1 == f . a & s1 == h0 . a ) by Def16;
then ( f . a == h0 . a & not emp f . a ) by A11, 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 A8, A12, 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 A8, A12, 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