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