let f be Function of NAT, 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 S₁[ set , set ] means c₂ in (coset the stack of X) /\ X;
A1: for x being set st x in Class (==_ X) holds
ex y being set st
( y in the carrier' of X & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in Class (==_ X) implies ex y being set st
( y in the carrier' of X & S₁[x,y] ) )
assume x in Class (==_ X) ; :: thesis: ex y being set st
( y in the carrier' of X & S₁[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 & S₁[x,s] )
thus s in the carrier' of X ; :: thesis: S₁[x,s]
thus s in (coset the stack of X) /\ x 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 set st x in Class (==_ X) holds
S₁[x,g . x] ) ) from FUNCT_1:sch 5(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 s = g . (f . i) by A6, FUNCT_2:15;
then s in (coset the stack of X) /\ (f . i) by A4, A5;
then A8: ( 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 A9: not emp S ; :: thesis: f . (i + 1) <> pop S
then A10: not emp s by Th36;
assume A11: f . (i + 1) = pop S ; :: thesis: contradiction
then A12: f . (i + 1) = Class ((==_ X),(pop s)) by A10, Th39;
set s3 = g . (f . (i + 1));
consider s4 being stack of X such that
A13: (coset the stack of X) /\ (f . (i + 1)) = {s4} by A12, Th33;
( pop s in coset the stack of X & pop s in pop S & pop S = f . (i + 1) ) by A8, A11, A10, Def17, Th39;
then A14: pop s in {s4} by A13, XBOOLE_0:def 4;
g . (f . (i + 1)) in (coset the stack of X) /\ (f . (i + 1)) by A4, A5;
then ( g . (f . (i + 1)) = s4 & pop s = s4 ) by A13, A14, TARSKI:def 1;
hence contradiction by A6, A9, Th36, FUNCT_2:15; :: thesis: verum