let X be StackAlgebra; :: thesis: for s1, s2 being stack of X st s1 == s2 & not emp s1 holds
top s1 = top s2
let s1, s2 be stack of X; :: thesis: ( s1 == s2 & not emp s1 implies top s1 = top s2 )
assume A1: ( s1 == s2 & not emp s1 ) ; :: thesis: top s1 = top s2
then A2: ( |.s1.| = |.s2.| & not emp s2 ) by Th14;
thus top s1 = |.s1.| . 1 by A1, Th9
.= top s2 by A2, Th9 ; :: thesis: verum