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;
A1: emp core s by Def19;
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;
( not emp push (e,s) & pop (push (e,s)) = s ) by Def11, Def12;
then [(push (e,s)),s] in ConstructionRed X by Def18;
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 A2, REWRITE1:8;
A4: v = <*(push (e,s))*> ^ t by REWRITE1:2;
then A5: v . 1 = push (e,s) by FINSEQ_1:41;
then reconsider v = v as the carrier' of X -valued RedSequence of ConstructionRed X by Th23;
A6: len <*(push (e,s))*> = 1 by FINSEQ_1:40;
then A7: len v = 1 + (len t) by A4, FINSEQ_1:22;
len t in dom t by FINSEQ_5:6;
then A8: v . (len v) = t . (len t) by A4, A6, A7, 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 A9: ( 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 A9, MSUALG_8:1;
then A10: ( v /. i = v . i & v /. (i + 1) = v . (i + 1) ) by PARTFUN1:def 6;
consider j being Nat such that
A11: i = 1 + j by A9, NAT_1:10;
A12: j < len t by A7, A9, A11, XREAL_1:6;

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

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

hence not emp v /. i by A5, A10, Def12; :: thesis: v /. (i + 1) = pop (v /. i)
1 in dom t by FINSEQ_5:6;
hence v /. (i + 1) = t . 1 by A4, A6, A10, A13, FINSEQ_1:def 7
.= pop (v /. i) by A13, A2, A5, A10, Def11 ;
:: thesis: verum

end;

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

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

end;

end;

end;

hence core (push (e,s)) = core s by A1, A2, A5, A8, Def19; :: thesis: verum