let X be StackAlgebra; for s being stack of X
for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds
( pop s in pop S & Class ((==_ X),(pop s)) = pop S )
let s be stack of X; for S being stack of (X /==) st S = Class ((==_ X),s) & not emp s holds
( pop s in pop S & Class ((==_ X),(pop s)) = pop S )
set p = the s_pop of X;
set i = id the s_empty of X;
let S be stack of (X /==); ( S = Class ((==_ X),s) & not emp s implies ( pop s in pop S & Class ((==_ X),(pop s)) = pop S ) )
assume A1:
S = Class ((==_ X),s)
; ( emp s or ( pop s in pop S & Class ((==_ X),(pop s)) = pop S ) )
assume A2:
not emp s
; ( pop s in pop S & Class ((==_ X),(pop s)) = pop S )
A3:
s in S
by A1, EQREL_1:20;
A4:
S in Class (==_ X)
by A1, EQREL_1:def 3;
A5:
dom (id the s_empty of X) = the s_empty of X
;
A6:
the s_pop of X +* (id the s_empty of X) is UnOp of the carrier' of X, ==_ X
A12:
s nin the s_empty of X
by A2;
pop S =
(( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X)) . S
by Def20
.=
Class ((==_ X),(( the s_pop of X +* (id the s_empty of X)) . s))
by A3, A4, A6, FILTER_1:def 3
.=
Class ((==_ X),(pop s))
by A5, A12, FUNCT_4:11
;
hence
( pop s in pop S & Class ((==_ X),(pop s)) = pop S )
by EQREL_1:20; verum