let X be StackAlgebra; :: thesis: for s being stack of X st not emp s holds
top s = |.s.| . 1
let s be stack of X; :: thesis: ( not emp s implies top s = |.s.| . 1 )
assume not emp s ; :: thesis: top s = |.s.| . 1
then |.s.| = <*(top s)*> ^ |.(pop s).| by Th6;
hence top s = |.s.| . 1 by FINSEQ_1:41; :: thesis: verum