scheme :: STACKS_1:sch 5
UNIQsch{ F1() -> StackAlgebra, F2() -> stack of F1(), F3() -> non empty set , F4() -> Element of F3(), F5( set , set ) -> Element of F3() } :
for a1, a2 being Element of F3() st ex F being Function of the carrier' of F1(),F3() st
( a1 = F . F2() & ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) ) & ex F being Function of the carrier' of F1(),F3() st
( a2 = F . F2() & ( for s1 being stack of F1() st emp s1 holds
F . s1 = F4() ) & ( for s1 being stack of F1()
for e being Element of F1() holds F . (push (e,s1)) = F5(e,(F . s1)) ) ) holds
a1 = a2