let X be StackAlgebra; 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; 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; ( s = t . 1 implies rng t c= coset s )
assume A1:
s = t . 1
; rng t c= coset s
then reconsider u = t as the carrier' of X -valued RedSequence of ConstructionRed X by Th23;
defpred S1[ Nat] means ( $1 in dom t implies t . $1 in coset s );
A2:
S1[ 0 ]
by FINSEQ_3:24;
A3:
now for i being Nat st S1[i] holds
S1[i + 1]let i be
Nat;
( S1[i] implies S1[i + 1] )assume A4:
S1[
i]
;
S1[i + 1]thus
S1[
i + 1]
verumproof
assume A5:
(
i + 1
in dom t &
t . (i + 1) nin coset s )
;
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;
verum
end; end;
A10:
for i being Nat holds S1[i]
from NAT_1:sch 2(A2, A3);
let x be object ; TARSKI:def 3 ( not x in rng t or x in coset s )
assume
x in rng t
; 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; verum