set X = StandardStackSystem A;
let s be stack of (StandardStackSystem A); :: according to STACKS_1:def 11 :: thesis: for e being Element of (StandardStackSystem A) holds s = pop (push (e,s))
let e be Element of (StandardStackSystem A); :: thesis: s = pop (push (e,s))
reconsider g = s as Element of A * by Def7;
reconsider h = push (e,s) as Element of A * by Def7;
A15: h = <*e*> ^ g by Def7;
then A16: not emp push (e,s) by Def7;
thus s = Del ((<*e*> ^ g),1) by WSIERP_1:40
.= pop (push (e,s)) by A15, A16, Def7 ; :: thesis: verum