let X be StackAlgebra; :: thesis: for s being stack of X st not emp s holds
core (pop s) = core s
let s be stack of X; :: thesis: ( not emp s implies core (pop s) = core s )
set R = ConstructionRed X;
set A = the carrier' of X;
assume A1: not emp s ; :: thesis: core (pop s) = core s
A2: emp core (pop s) by Def19;
consider t being the carrier' of X -valued RedSequence of ConstructionRed X such that
A3: ( t . 1 = pop s & t . (len t) = core (pop s) ) and
A4: for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) by Def19;
[s,(pop s)] in ConstructionRed X by A1, Def18;
then reconsider u = <*s,(pop s)*> as RedSequence of ConstructionRed X by REWRITE1:7;
( u . 2 = pop s & len u = 2 ) by FINSEQ_1:44;
then reconsider v = u $^ t as RedSequence of ConstructionRed X by A3, REWRITE1:8;
A5: v = <*s*> ^ t by REWRITE1:2;
then A6: v . 1 = s by FINSEQ_1:41;
then reconsider v = v as the carrier' of X -valued RedSequence of ConstructionRed X by Th23;
A7: len <*s*> = 1 by FINSEQ_1:40;
then A8: len v = 1 + (len t) by A5, FINSEQ_1:22;
len t in dom t by FINSEQ_5:6;
then A9: v . (len v) = t . (len t) by A5, A7, A8, FINSEQ_1:def 7;

now :: thesis: for i being Nat st 1 <= i & i < len v holds
( not emp v /. i & v /. (i + 1) = pop (v /. i) )

let i be Nat; :: thesis: ( 1 <= i & i < len v implies ( not emp v /. b₁ & v /. (b₁ + 1) = pop (v /. b₁) ) )
assume A10: ( 1 <= i & i < len v ) ; :: thesis: ( not emp v /. b₁ & v /. (b₁ + 1) = pop (v /. b₁) )
( i in dom v & i + 1 in dom v ) by A10, MSUALG_8:1;
then A11: ( v /. i = v . i & v /. (i + 1) = v . (i + 1) ) by PARTFUN1:def 6;
consider j being Nat such that
A12: i = 1 + j by A10, NAT_1:10;
A13: j < len t by A8, A10, A12, XREAL_1:6;

per cases ( i = 1 or i > 1 ) by A10, XXREAL_0:1;

suppose A14: i = 1 ; :: thesis: ( not emp v /. b₁ & v /. (b₁ + 1) = pop (v /. b₁) )

hence not emp v /. i by A1, A5, A11, FINSEQ_1:41; :: thesis: v /. (i + 1) = pop (v /. i)
1 in dom t by FINSEQ_5:6;
hence v /. (i + 1) = t . 1 by A5, A7, A11, A14, FINSEQ_1:def 7
.= pop (v /. i) by A14, A3, A5, A11, FINSEQ_1:41 ;
:: thesis: verum

end;

suppose i > 1 ; :: thesis: ( not emp v /. b₁ & v /. (b₁ + 1) = pop (v /. b₁) )

then A15: ( j >= 1 & j in NAT ) by A12, NAT_1:13, ORDINAL1:def 12;
then ( j in dom t & i in dom t ) by A12, A13, MSUALG_8:1;
then ( t . j = v . i & t /. j = t . j & t . i = v . (i + 1) & t /. i = t . i ) by A5, A7, A12, FINSEQ_1:def 7, PARTFUN1:def 6;
hence ( not emp v /. i & v /. (i + 1) = pop (v /. i) ) by A4, A11, A12, A13, A15; :: thesis: verum

end;

end;

end;

hence core (pop s) = core s by A2, A3, A6, A9, Def19; :: thesis: verum