let X be StackAlgebra; for s being stack of X
for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds
top S = top s
let s be stack of X; for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds
top S = top s
set t = the s_top of X;
set A = the s_empty of X;
set e = the Element of the carrier of X;
let S be stack of (X /==); ( S = Class ((==_ X),s) & not emp s implies top S = top s )
assume A1:
S = Class ((==_ X),s)
; ( emp s or top S = top s )
assume A2:
not emp s
; top S = top s
then
not emp S
by A1, Th36;
then A3:
S <> the s_empty of X
by Th37;
set f = the Choice_Function of (Class (==_ X));
A4:
( S in Class (==_ X) & {} nin Class (==_ X) )
by A1, EQREL_1:def 3;
then A5:
the Choice_Function of (Class (==_ X)) . S in S
by ORDERS_1:89;
then reconsider x = the Choice_Function of (Class (==_ X)) . S as stack of X by A1;
[s,x] in ==_ X
by A1, A5, EQREL_1:18;
then A6:
s == x
by Def16;
A7:
dom the Choice_Function of (Class (==_ X)) = Class (==_ X)
by A4, RLVECT_3:28;
the s_top of (X /==) = ( the s_top of X * the Choice_Function of (Class (==_ X))) +* ( the s_empty of X, the Element of the carrier of X)
by Def20;
hence top S =
( the s_top of X * the Choice_Function of (Class (==_ X))) . S
by A3, FUNCT_7:32
.=
top x
by A4, A7, FUNCT_1:13
.=
top s
by A6, A2, Th18
;
verum