set X = StandardStackSystem A;
let s be stack of (StandardStackSystem A); :: according to STACKS_1:def 10 :: thesis: for e being Element of (StandardStackSystem A) holds e = top (push (e,s))
let e be Element of (StandardStackSystem A); :: thesis: e = top (push (e,s))
reconsider g = s as Element of A * by EXAM;
reconsider h = push (e,s) as Element of A * by EXAM;
A1: h = <*e*> ^ g by EXAM;
then A2: not emp push (e,s) by EXAM;
thus e = h . 1 by A1, FINSEQ_1:41
.= top (push (e,s)) by A2, EXAM ; :: thesis: verum