let X be StackAlgebra; :: thesis: 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; :: thesis: 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 /==); :: thesis: ( S = Class ((==_ X),s) & not emp s implies ( pop s in pop S & Class ((==_ X),(pop s)) = pop S ) )
assume Z0: S = Class ((==_ X),s) ; :: thesis: ( emp s or ( pop s in pop S & Class ((==_ X),(pop s)) = pop S ) )
assume Z1: not emp s ; :: thesis: ( pop s in pop S & Class ((==_ X),(pop s)) = pop S )
A1: s in S by Z0, EQREL_1:20;
A2: S in Class (==_ X) by Z0, EQREL_1:def 3;
A6: dom (id the s_empty of X) = the s_empty of X by RELAT_1:45;
A3: the s_pop of X +* (id the s_empty of X) is UnOp of the carrier' of X, ==_ X

proof

let y1, y2 be stack of X; :: according to FILTER_1:def 1 :: thesis: ( not [y1,y2] in ==_ X or [(( the s_pop of X +* (id the s_empty of X)) . y1),(( the s_pop of X +* (id the s_empty of X)) . y2)] in ==_ X )
assume B1: [y1,y2] in ==_ X ; :: thesis: [(( the s_pop of X +* (id the s_empty of X)) . y1),(( the s_pop of X +* (id the s_empty of X)) . y2)] in ==_ X
then A4: y1 == y2 by REL;

per cases ( not emp y1 or emp y1 ) ;

suppose A5: not emp y1 ; :: thesis: [(( the s_pop of X +* (id the s_empty of X)) . y1),(( the s_pop of X +* (id the s_empty of X)) . y2)] in ==_ X

then not emp y2 by A4, Th42;
then ( y1 nin the s_empty of X & y2 nin the s_empty of X ) by A5, EMP;
then A7: ( ( the s_pop of X +* (id the s_empty of X)) . y1 = the s_pop of X . y1 & ( the s_pop of X +* (id the s_empty of X)) . y2 = the s_pop of X . y2 ) by A6, FUNCT_4:11;
pop y1 == pop y2 by A4, A5, Th45;
hence [(( the s_pop of X +* (id the s_empty of X)) . y1),(( the s_pop of X +* (id the s_empty of X)) . y2)] in ==_ X by A7, REL; :: thesis: verum

end;

suppose A5: emp y1 ; :: thesis: [(( the s_pop of X +* (id the s_empty of X)) . y1),(( the s_pop of X +* (id the s_empty of X)) . y2)] in ==_ X

then emp y2 by A4, Th42;
then ( y1 in the s_empty of X & y2 in the s_empty of X ) by A5, EMP;
then ( ( the s_pop of X +* (id the s_empty of X)) . y1 = (id the s_empty of X) . y1 & (id the s_empty of X) . y1 = y1 & ( the s_pop of X +* (id the s_empty of X)) . y2 = (id the s_empty of X) . y2 & (id the s_empty of X) . y2 = y2 ) by A6, FUNCT_1:18, FUNCT_4:13;
hence [(( the s_pop of X +* (id the s_empty of X)) . y1),(( the s_pop of X +* (id the s_empty of X)) . y2)] in ==_ X by B1; :: thesis: verum

end;

end;

end;

A8: s nin the s_empty of X by Z1, EMP;
pop S = (( the s_pop of X +* (id the s_empty of X)) /\/ (==_ X)) . S by QUOT
.= Class ((==_ X),(( the s_pop of X +* (id the s_empty of X)) . s)) by A1, A2, A3, FILTER_1:def 3
.= Class ((==_ X),(pop s)) by A6, A8, FUNCT_4:11 ;
hence ( pop s in pop S & Class ((==_ X),(pop s)) = pop S ) by EQREL_1:20; :: thesis: verum