let X be StackAlgebra; :: thesis: for s being stack of X
for e being Element of X holds core (push (e,s)) = core s
let s be stack of X; :: thesis: for e being Element of X holds core (push (e,s)) = core s
let e be Element of X; :: thesis: core (push (e,s)) = core s
set R = ConstructionRed X;
set A = the carrier' of X;
A0: emp core s by CORE;
consider t being the carrier' of X -valued RedSequence of ConstructionRed X such that
A1: ( t . 1 = s & t . (len t) = core 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;
( not emp push (e,s) & pop (push (e,s)) = s ) by POPPUSH, PUSHNE;
then [(push (e,s)),s] in ConstructionRed X by CRED;
then reconsider u = <*(push (e,s)),s*> as RedSequence of ConstructionRed X by REWRITE1:7;
( u . 2 = s & len u = 2 ) by FINSEQ_1:44;
then reconsider v = u $^ t as RedSequence of ConstructionRed X by A1, REWRITE1:8;
A3: v = <*(push (e,s))*> ^ t by REWRITE1:2;
then A4: v . 1 = push (e,s) by FINSEQ_1:41;
then reconsider v = v as the carrier' of X -valued RedSequence of ConstructionRed X by Lem2;
A7: len <*(push (e,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 A4, B3, PUSHNE; :: 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, A4, B3, POPPUSH ;
:: 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 (push (e,s)) = core s by A0, A1, A4, A6, CORE; :: thesis: verum