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
B2: x = Class ((==_ X),s2) by EQREL_1:36;
consider s being stack of X such that
B3: (coset the stack of X) /\ (Class ((==_ X),s2)) = {s} by Th60;
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 B2, B3, TARSKI:def 1; :: thesis: verum

end;

consider g being Function such that
A2: ( 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);
A4: the carrier' of (X /==) = Class (==_ X) by QUOT;
then reconsider g = g as Function of the carrier' of (X /==), the carrier' of X by A2, FUNCT_2:2;
consider i being Nat, s being stack of X such that
A3: ( (g * f) . i = s & ( not emp s implies (g * f) . (i + 1) <> pop s ) ) by POPFIN;
reconsider S = Class ((==_ X),s) as stack of (X /==) by A4, 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
A5: f . i = Class ((==_ X),s2) by A4, EQREL_1:36;
i in NAT by ORDINAL1:def 12;
then s = g . (f . i) by A3, FUNCT_2:15;
then s in (coset the stack of X) /\ (f . i) by A2, A4;
then A6: ( s in coset the stack of X & s in f . i ) by XBOOLE_0:def 4;
hence f . i = S by A5, EQREL_1:23; :: thesis: ( not emp S implies f . (i + 1) <> pop S )
assume B2: not emp S ; :: thesis: f . (i + 1) <> pop S
then A8: not emp s by Th71;
assume B1: f . (i + 1) = pop S ; :: thesis: contradiction
then A9: f . (i + 1) = Class ((==_ X),(pop s)) by A8, Th73;
set s3 = g . (f . (i + 1));
consider s4 being stack of X such that
A10: (coset the stack of X) /\ (f . (i + 1)) = {s4} by A9, Th60;
( pop s in coset the stack of X & pop s in pop S & pop S = f . (i + 1) ) by A6, B1, A8, COSET, Th73;
then A11: pop s in {s4} by A10, XBOOLE_0:def 4;
g . (f . (i + 1)) in (coset the stack of X) /\ (f . (i + 1)) by A2, A4;
then ( g . (f . (i + 1)) = s4 & pop s = s4 ) by A10, A11, TARSKI:def 1;
hence contradiction by A3, B2, Th71, FUNCT_2:15; :: thesis: verum