let X be StackAlgebra; :: thesis: for s being stack of X
for e being Element of X holds |.(push (e,s)).| = <*e*> ^ |.s.|
let s be stack of X; :: thesis: for e being Element of X holds |.(push (e,s)).| = <*e*> ^ |.s.|
let e be Element of X; :: thesis: |.(push (e,s)).| = <*e*> ^ |.s.|
not emp push (e,s) by Def12;
hence |.(push (e,s)).| = <*(top (push (e,s)))*> ^ |.(pop (push (e,s))).| by Th6
.= <*e*> ^ |.(pop (push (e,s))).| by Def10
.= <*e*> ^ |.s.| by Def11 ;
:: thesis: verum