let X be StackAlgebra; for s being stack of X st emp s holds
core s = s
let s be stack of X; ( emp s implies core s = s )
set R = ConstructionRed X;
assume A1:
emp s
; core s = s
consider t being the carrier' of X -valued RedSequence of ConstructionRed X such that
A2:
( t . 1 = s & t . (len t) = core s )
and
A3:
for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) )
by Def19;
A4:
1 in dom t
by FINSEQ_5:6;
then
t /. 1 = t . 1
by PARTFUN1:def 6;
then
( 1 <= len t & len t <= 1 )
by A1, A2, A3, A4, FINSEQ_3:25;
hence
core s = s
by A2, XXREAL_0:1; verum