let f be sequence of the carrier' of (X /==); :: according to STACKS_1:def 8 :: thesis: ex i being Nat ex s being stack of (X /==) st
( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) )
set s1 = the stack of X;
defpred S1[ object , object ] means ex B being set st
( B = X & c2 in (coset the stack of X) /\ B );
A1: for x being object st x in Class (==_ X) holds
ex y being object st
( y in the carrier' of X & S1[x,y] )
proof
let x be object ; :: thesis: ( x in Class (==_ X) implies ex y being object st
( y in the carrier' of X & S1[x,y] ) )
assume x in Class (==_ X) ; :: thesis: ex y being object st
( y in the carrier' of X & S1[x,y] )
then consider s2 being stack of X such that
A2: x = Class ((==_ X),s2) by EQREL_1:36;
consider s being stack of X such that
A3: (coset the stack of X) /\ (Class ((==_ X),s2)) = {s} by Th33;
take s ; :: thesis: ( s in the carrier' of X & S1[x,s] )
thus s in the carrier' of X ; :: thesis: S1[x,s]
reconsider B = x as set by TARSKI:1;
take B ; :: thesis: ( B = x & s in (coset the stack of X) /\ B )
thus B = x ; :: thesis: s in (coset the stack of X) /\ B
thus s in (coset the stack of X) /\ B by A2, A3, TARSKI:def 1; :: thesis: verum
end;
consider g being Function such that
A4: ( dom g = Class (==_ X) & rng g c= the carrier' of X & ( for x being object st x in Class (==_ X) holds
S1[x,g . x] ) ) from FUNCT_1:sch 6(A1);
 A5: the carrier' of (X /==) = Class (==_ X) by Def20;
then reconsider g = g as Function of the carrier' of (X /==), the carrier' of X by A4, FUNCT_2:2;
consider i being Nat, s being stack of X such that
A6: ( (g * f) . i = s & ( not emp s implies (g * f) . (i + 1) <> pop s ) ) by Def8;
reconsider S = Class ((==_ X),s) as stack of (X /==) by A5, EQREL_1:def 3;
take i ; :: thesis: ex s being stack of (X /==) st
( f . i = s & ( not emp s implies f . (i + 1) <> pop s ) )
take S ; :: thesis: ( f . i = S & ( not emp S implies f . (i + 1) <> pop S ) )
consider s2 being stack of X such that
A7: f . i = Class ((==_ X),s2) by A5, EQREL_1:36;
i in NAT by ORDINAL1:def 12;
then A8: s = g . (f . i) by A6, FUNCT_2:15;
S1[f . i,g . (f . i)] by A4, A5;
then s in (coset the stack of X) /\ (f . i) by A8;
then A9: ( s in coset the stack of X & s in f . i ) by XBOOLE_0:def 4;
hence f . i = S by A7, EQREL_1:23; :: thesis: ( not emp S implies f . (i + 1) <> pop S )
assume A10: not emp S ; :: thesis: f . (i + 1) <> pop S
then A11: not emp s by Th36;
assume A12: f . (i + 1) = pop S ; :: thesis: contradiction
then A13: f . (i + 1) = Class ((==_ X),(pop s)) by A11, Th39;
set s3 = g . (f . (i + 1));
consider s4 being stack of X such that
A14: (coset the stack of X) /\ (f . (i + 1)) = {s4} by A13, Th33;
( pop s in coset the stack of X & pop s in pop S & pop S = f . (i + 1) ) by A9, A12, A11, Def17, Th39;
then A15: pop s in {s4} by A14, XBOOLE_0:def 4;
S1[f . (i + 1),g . (f . (i + 1))] by A4, A5;
then g . (f . (i + 1)) in (coset the stack of X) /\ (f . (i + 1)) ;
then ( g . (f . (i + 1)) = s4 & pop s = s4 ) by A14, A15, TARSKI:def 1;
hence contradiction by A6, A10, Th36, FUNCT_2:15; :: thesis: verum