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)) #); ( 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; 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)); 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 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)) . alet a be
Element of
Class (==_ X);
(( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . b1 = (( the s_top of X * h0) +* ( the s_empty of X, the Element of the carrier of X)) . b1consider 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 A11:
not
emp s1
;
(( the s_top of X * f) +* ( the s_empty of X, the Element of the carrier of X)) . b1 = (( the s_top of X * h0) +* ( the s_empty of X, the Element of the carrier of X)) . b1then
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;
verum 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; verum