let X be StackAlgebra; :: thesis: for s being stack of X st not emp s holds
|.s.| = <*(top s)*> ^ |.(pop s).|
let s be stack of X; :: thesis: ( not emp s implies |.s.| = <*(top s)*> ^ |.(pop s).| )
consider F being Function of the carrier' of X,( the carrier of X *) such that
A1: ( |.s.| = F . s & ( for s1 being stack of X st emp s1 holds
F . s1 = {} ) & ( for s1 being stack of X
for e being Element of X holds F . (push (e,s1)) = <*e*> ^ (F . s1) ) ) by Def13;
A2: |.(pop s).| = F . (pop s) by A1, Def13;
assume not emp s ; :: thesis: |.s.| = <*(top s)*> ^ |.(pop s).|
then s = push ((top s),(pop s)) by Def9;
hence |.s.| = <*(top s)*> ^ |.(pop s).| by A1, A2; :: thesis: verum