scheme :: STACKS_1:sch 4
EXsch{ F₁() -> StackAlgebra, F₂() -> stack of F₁(), F₃() -> non empty set , F₄() -> Element of F₃(), F₅( set , set ) -> Element of F₃() } :

ex a being Element of F₃() ex F being Function of the carrier' of F₁(),F₃() st
( a = F . F₂() & ( for s1 being stack of F₁() st emp s1 holds
F . s1 = F₄() ) & ( for s1 being stack of F₁()
for e being Element of F₁() holds F . (push (e,s1)) = F₅(e,(F . s1)) ) )