let X be StackAlgebra; :: thesis: for s1, s2 being stack of X
for e being Element of X st s1 == s2 holds
push (e,s1) == push (e,s2)
let s1, s2 be stack of X; :: thesis: for e being Element of X st s1 == s2 holds
push (e,s1) == push (e,s2)
let e be Element of X; :: thesis: ( s1 == s2 implies push (e,s1) == push (e,s2) )
assume |.s1.| = |.s2.| ; :: according to STACKS_1:def 14 :: thesis: push (e,s1) == push (e,s2)
hence |.(push (e,s1)).| = <*e*> ^ |.s2.| by Th8
.= |.(push (e,s2)).| by Th8 ;
:: according to STACKS_1:def 14 :: thesis: verum