let X be StackAlgebra; 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; 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
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 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;
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;
( 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 }
;
( 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 }
;
( not emp s2 implies pop s2 in { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } )assume
not
emp s2
;
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 }
;
verum end;
hence
coset s c= { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 }
by A1, A2, Def17; XBOOLE_0:def 10 { s1 where s1 is stack of X : ConstructionRed X reduces s,s1 } c= coset s
let x be object ; TARSKI:def 3 ( 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 }
; 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
; verum