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 AA: not emp s ; :: thesis: core (pop s) = core s
A0: emp core (pop s) by CORE;
consider t being the carrier' of X -valued RedSequence of ConstructionRed X such that
A1: ( t . 1 = pop s & t . (len t) = core (pop s) ) and
A2: for i being Nat st 1 <= i & i < len t holds
( not emp t /. i & t /. (i + 1) = pop (t /. i) ) by CORE;
[s,(pop s)] in ConstructionRed X by AA, CRED;
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 A1, REWRITE1:8;
A3: v = <*s*> ^ t by REWRITE1:2;
then A4: v . 1 = s by FINSEQ_1:41;
then reconsider v = v as the carrier' of X -valued RedSequence of ConstructionRed X by Lem2;
A7: len <*s*> = 1 by FINSEQ_1:40;
then A5: len v = 1 + (len t) by A3, FINSEQ_1:22;
len t in dom t by FINSEQ_5:6;
then A6: v . (len v) = t . (len t) by A3, A7, A5, FINSEQ_1:def 7;

now

let i be Nat; :: thesis: ( 1 <= i & i < len v implies ( not emp v /. b₁ & v /. (b₁ + 1) = pop (v /. b₁) ) )
assume B1: ( 1 <= i & i < len v ) ; :: thesis: ( not emp v /. b₁ & v /. (b₁ + 1) = pop (v /. b₁) )
i in NAT by ORDINAL1:def 12;
then ( i in dom v & i + 1 in dom v ) by B1, MSUALG_8:1;
then B3: ( v /. i = v . i & v /. (i + 1) = v . (i + 1) ) by PARTFUN1:def 6;
consider j being Nat such that
B4: i = 1 + j by B1, NAT_1:10;
B5: j < len t by A5, B1, B4, XREAL_1:6;

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

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

hence not emp v /. i by AA, A3, B3, 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 A3, A7, B3, C1, FINSEQ_1:def 7
.= pop (v /. i) by C1, A1, A3, B3, FINSEQ_1:41 ;
:: thesis: verum

end;

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

then B6: ( j >= 1 & j in NAT ) by B4, NAT_1:13, ORDINAL1:def 12;
then ( j in dom t & i in dom t ) by B4, B5, MSUALG_8:1;
then ( t . j = v . i & t /. j = t . j & t . i = v . (i + 1) & t /. i = t . i ) by A3, A7, B4, FINSEQ_1:def 7, PARTFUN1:def 6;
hence ( not emp v /. i & v /. (i + 1) = pop (v /. i) ) by A2, B3, B4, B5, B6; :: thesis: verum

end;

end;

end;

hence core (pop s) = core s by A0, A1, A4, A6, CORE; :: thesis: verum