let X be StackAlgebra; for s1, s2 being stack of X st s1 == s2 & not emp s1 holds
pop s1 == pop s2
let s1, s2 be stack of X; ( s1 == s2 & not emp s1 implies pop s1 == pop s2 )
assume A1:
( s1 == s2 & not emp s1 )
; pop s1 == pop s2
then A2:
( |.s1.| = |.s2.| & not emp s2 )
by Th14;
thus |.(pop s1).| =
Del (|.s1.|,1)
by A1, Th7
.=
|.(pop s2).|
by A2, Th7
; STACKS_1:def 14 verum