let X be StackAlgebra; :: thesis: for s being stack of X st emp s holds
|.s.| = {}
let s be stack of X; :: thesis: ( emp s implies |.s.| = {} )
ex F being Function of the carrier' of X,( the carrier of X *) st
( |.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;
hence ( emp s implies |.s.| = {} ) ; :: thesis: verum