let X be StackAlgebra; 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; 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; 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 /==); 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 /==); ( 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)
; ( not E = e or ( push (e,s) in push (E,S) & Class ((==_ X),(push (e,s))) = push (E,S) ) )
assume A2:
E = e
; ( 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;
STACKS_1:def 1 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 ==_ Xlet y1,
y2 be
stack of
X;
( [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
;
[( 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;
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; verum