set X = StandardStackSystem A;
let s be stack of (StandardStackSystem A); STACKS_1:def 9 ( not emp s implies s = push ((top s),(pop s)) )
reconsider g = s as Element of A * by Def7;
assume A10:
not emp s
; s = push ((top s),(pop s))
then A11:
not s is empty
by Def7;
then A12:
g = <*(g . 1)*> ^ (Del (g,1))
by FINSEQ_5:86;
reconsider h = Del (g,1) as stack of (StandardStackSystem A) by Def7;
1 in dom g
by A11, FINSEQ_5:6;
then
g . 1 in A
by FUNCT_1:102;
then reconsider x = g . 1 as Element of (StandardStackSystem A) by Def7;
thus s =
push (x,h)
by A12, Def7
.=
push ((top s),h)
by A10, Def7
.=
push ((top s),(pop s))
by A10, Def7
; verum