:: deftheorem Def13 defines |. STACKS_1:def 13 :
for X being StackAlgebra
for s being stack of X
for b₃ being Element of the carrier of X * holds
( b₃ = |.s.| iff ex F being Function of the carrier' of X,( the carrier of X *) st
( b₃ = 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) ) ) );