let X be StackAlgebra; :: thesis: for s being stack of X
for t being RedSequence of ConstructionRed X st s = t . 1 holds
rng t c= coset s
let s be stack of X; :: thesis: for t being RedSequence of ConstructionRed X st s = t . 1 holds
rng t c= coset s
set R = ConstructionRed X;
let t be RedSequence of ConstructionRed X; :: thesis: ( s = t . 1 implies rng t c= coset s )
assume A1: s = t . 1 ; :: thesis: rng t c= coset s
then reconsider u = t as the carrier' of X -valued RedSequence of ConstructionRed X by Th23;
defpred S₁[ Nat] means ( $1 in dom t implies t . $1 in coset s );
A2: S₁[ 0 ] by FINSEQ_3:24;

A3: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
thus S₁[i + 1] :: thesis: verum

proof

assume A5: ( i + 1 in dom t & t . (i + 1) nin coset s ) ; :: thesis: contradiction
( i = 0 or i >= 0 + 1 ) by NAT_1:13;
then consider j being Nat such that
A6: i = j + 1 by A1, A5, Def17, NAT_1:6;
( i <= i + 1 & i + 1 <= len t ) by A5, FINSEQ_3:25, NAT_1:11;
then A7: ( 1 <= i & i <= len t & rng t <> {} ) by A6, NAT_1:11, XXREAL_0:2;
then A8: ( i in dom t & 1 in dom t ) by FINSEQ_3:25, FINSEQ_3:32;
then A9: ( t . i = u /. i & t . (i + 1) = u /. (i + 1) ) by A5, PARTFUN1:def 6;
then [(u /. i),(u /. (i + 1))] in ConstructionRed X by A5, A8, REWRITE1:def 2;
then ( ( not emp u /. i & u /. (i + 1) = pop (u /. i) ) or ex e being Element of X st u /. (i + 1) = push (e,(u /. i)) ) by Def18;
hence contradiction by A4, A5, A7, A9, Def17, FINSEQ_3:25; :: thesis: verum

end;

end;

A10: for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng t or x in coset s )
assume x in rng t ; :: thesis: x in coset s
then ex y being object st
( y in dom t & x = t . y ) by FUNCT_1:def 3;
hence x in coset s by A10; :: thesis: verum