theorem Th8: :: STACKS_1:8

for X being StackAlgebra
for s being stack of X
for e being Element of X holds |.(push (e,s)).| = <*e*> ^ |.s.|