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 A1: S = Class ((==_ X),s) ; :: thesis: ( emp s or ( pop s in pop S & Class ((==_ X),(pop s)) = pop S ) )
assume A2: not emp s ; :: thesis: ( 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

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 A7: [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 A8: y1 == y2 by Def16;

per cases ( not emp y1 or emp y1 ) ;

suppose A9: 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 A8, Th14;
then ( y1 nin the s_empty of X & y2 nin the s_empty of X ) by A9;
then A10: ( ( 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 A5, FUNCT_4:11;
pop y1 == pop y2 by A8, A9, Th17;
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 A10, Def16; :: thesis: verum

end;

suppose A11: 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 A8, Th14;
then ( y1 in the s_empty of X & y2 in the s_empty of X ) by A11;
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 A5, 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 A7; :: thesis: verum

end;

end;

end;

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; :: thesis: verum