let X be StackAlgebra; :: thesis: for s being stack of X
for e being Element of X
for S being stack of (X /==)
for E being Element of (X /==) st S = Class ((==_ X),s) & E = e holds
( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) )
let s be stack of X; :: thesis: for e being Element of X
for S being stack of (X /==)
for E being Element of (X /==) st S = Class ((==_ X),s) & E = e holds
( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) )
let e be Element of X; :: thesis: for S being stack of (X /==)
for E being Element of (X /==) st S = Class ((==_ X),s) & E = e holds
( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) )
let S be stack of (X /==); :: thesis: for E being Element of (X /==) st S = Class ((==_ X),s) & E = e holds
( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) )
let E be Element of (X /==); :: thesis: ( S = Class ((==_ X),s) & E = e implies ( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) ) )
assume A1: S = Class ((==_ X),s) ; :: thesis: ( not E = e or ( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) ) )
assume A2: E = e ; :: thesis: ( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) )
A3: s in S by A1, EQREL_1:20;
A4: S in Class (==_ X) by A1, EQREL_1:def 3;
A5: the s_push of X is BinOp of the carrier of X, the carrier' of X, ==_ X

proof

let x be Element of X; :: according to STACKS_1:def 1 :: thesis: for y1, y2 being Element of the carrier' of X st [y1,y2] in ==_ X holds
[( the s_push of X . (x,y1)),( the s_push of X . (x,y2))] in ==_ X
let y1, y2 be stack of X; :: thesis: ( [y1,y2] in ==_ X implies [( the s_push of X . (x,y1)),( the s_push of X . (x,y2))] in ==_ X )
assume [y1,y2] in ==_ X ; :: thesis: [( the s_push of X . (x,y1)),( the s_push of X . (x,y2))] in ==_ X
then y1 == y2 by Def16;
then push (x,y1) == push (x,y2) by Th16;
hence [( the s_push of X . (x,y1)),( the s_push of X . (x,y2))] in ==_ X by Def16; :: thesis: verum

end;

push (E,S) = ( the s_push of X /\/ (==_ X)) . (E,S) by Def20
.= Class ((==_ X),(push (e,s))) by A2, A3, A4, A5, Def2 ;
hence ( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) ) by EQREL_1:20; :: thesis: verum