for X being StackAlgebra
for s being stack of X st not emp s holds
|.s.| = <*(top s)*> ^ |.(pop s).|