let X be StackAlgebra; :: thesis: for s being stack of X holds coset s = { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 }
let s be stack of X; :: thesis: coset s = { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 }
set R = ConstructionRed X;
A1: { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } c= the carrier' of X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } or x in the carrier' of X )
assume x in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } ; :: thesis: x in the carrier' of X
then ex s1 being stack of X st
( x = s1 & ConstructionRed X reduces s,s1 ) ;
hence x in the carrier' of X ; :: thesis: verum

end;

ConstructionRed X reduces s,s by REWRITE1:12;
then A2: s in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } ;

now :: thesis: for e being Element of X
for s2 being stack of X st s2 in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } holds
( push (e,s2) in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } & ( not emp s2 implies pop s2 in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } ) )

let e be Element of X; :: thesis: for s2 being stack of X st s2 in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } holds
( push (e,s2) in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } & ( not emp s2 implies pop s2 in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } ) )
let s2 be stack of X; :: thesis: ( s2 in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } implies ( push (e,s2) in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } & ( not emp s2 implies pop s2 in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } ) ) )
assume s2 in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } ; :: thesis: ( push (e,s2) in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } & ( not emp s2 implies pop s2 in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } ) )
then A3: ex s1 being stack of X st
( s2 = s1 & ConstructionRed X reduces s,s1 ) ;
[s2,(push (e,s2))] in ConstructionRed X by Def18;
then ConstructionRed X reduces s2, push (e,s2) by REWRITE1:15;
then ConstructionRed X reduces s, push (e,s2) by A3, REWRITE1:16;
hence push (e,s2) in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } ; :: thesis: ( not emp s2 implies pop s2 in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } )
assume not emp s2 ; :: thesis: pop s2 in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 }
then [s2,(pop s2)] in ConstructionRed X by Def18;
then ConstructionRed X reduces s2, pop s2 by REWRITE1:15;
then ConstructionRed X reduces s, pop s2 by A3, REWRITE1:16;
hence pop s2 in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } ; :: thesis: verum

end;

hence coset s c= { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } by A1, A2, Def17; :: according to XBOOLE_0:def 10 :: thesis: { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } c= coset s
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } or x in coset s )
assume x in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } ; :: thesis: x in coset s
then consider s1 being stack of X such that
A4: ( x = s1 & ConstructionRed X reduces s,s1 ) ;
consider t being RedSequence of ConstructionRed X such that
A5: ( s = t . 1 & s1 = t . (len t) ) by A4;
len t in dom t by FINSEQ_5:6;
then ( x in rng t & rng t c= coset s ) by A4, A5, Th24, FUNCT_1:def 3;
hence x in coset s ; :: thesis: verum