set X = StandardStackSystem A;
let s be stack of (StandardStackSystem A); :: according to STACKS_1:def 9 :: thesis: ( not emp s implies s = push ((top s),(pop s)) )
reconsider g = s as Element of A * by EXAM;
assume A0: not emp s ; :: thesis: s = push ((top s),(pop s))
then A2: not s is empty by EXAM;
then A1: g = <*(g . 1)*> ^ (Del (g,1)) by POLYALG1:4;
reconsider h = Del (g,1) as stack of (StandardStackSystem A) by EXAM;
1 in dom g by A2, FINSEQ_5:6;
then g . 1 in A by FUNCT_1:102;
then reconsider x = g . 1 as Element of (StandardStackSystem A) by EXAM;
thus s = push (x,h) by A1, EXAM
.= push ((top s),h) by A0, EXAM
.= push ((top s),(pop s)) by A0, EXAM ; :: thesis: verum