let E be non empty set ; :: thesis: for e being Element of E
for u being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)}
for R being RedSequence of ==>.-relation TS st (R . 1) `2 = <%e%> ^ u & (R . (len R)) `2 = <%> E & not (R . 2) `2 = <%e%> ^ u holds
(R . 2) `2 = u
let e be Element of E; :: thesis: for u being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)}
for R being RedSequence of ==>.-relation TS st (R . 1) `2 = <%e%> ^ u & (R . (len R)) `2 = <%> E & not (R . 2) `2 = <%e%> ^ u holds
(R . 2) `2 = u
let u be Element of E ^omega ; :: thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)}
for R being RedSequence of ==>.-relation TS st (R . 1) `2 = <%e%> ^ u & (R . (len R)) `2 = <%> E & not (R . 2) `2 = <%e%> ^ u holds
(R . 2) `2 = u
let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; :: thesis: for R being RedSequence of ==>.-relation TS st (R . 1) `2 = <%e%> ^ u & (R . (len R)) `2 = <%> E & not (R . 2) `2 = <%e%> ^ u holds
(R . 2) `2 = u
let R be RedSequence of ==>.-relation TS; :: thesis: ( (R . 1) `2 = <%e%> ^ u & (R . (len R)) `2 = <%> E & not (R . 2) `2 = <%e%> ^ u implies (R . 2) `2 = u )
assume that
A1: (R . 1) `2 = <%e%> ^ u and
A2: (R . (len R)) `2 = <%> E ; :: thesis: ( (R . 2) `2 = <%e%> ^ u or (R . 2) `2 = u )
(R . 1) `2 <> (R . (len R)) `2 by A1, A2, AFINSQ_1:30;
then len R >= 1 + 1 by NAT_1:8, NAT_1:25;
then ( rng R <> {} & 1 + 1 in dom R ) by FINSEQ_3:25;
then A3: [(R . 1),(R . 2)] in ==>.-relation TS by FINSEQ_3:32, REWRITE1:def 2;
then consider p being Element of TS, v being Element of E ^omega , q being Element of TS, w being Element of E ^omega such that
A4: R . 1 = [p,v] and
A5: R . 2 = [q,w] by REWRITE3:31;
p,v ==>. q,w,TS by A3, A4, A5, REWRITE3:def 4;
then consider u1 being Element of E ^omega such that
A6: p,u1 -->. q,TS and
A7: v = u1 ^ w by REWRITE3:22;
A8: u1 in (Lex E) \/ {(<%> E)} by A6, REWRITE3:15;

per cases ( u1 in Lex E or u1 in {(<%> E)} ) by A8, XBOOLE_0:def 3;

suppose u1 in Lex E ; :: thesis: ( (R . 2) `2 = <%e%> ^ u or (R . 2) `2 = u )

then len u1 = 1 by Th9;
then consider f being Element of E such that
A9: u1 = <%f%> and
u1 . 0 = f by Th4;
(R . 1) `2 = <%f%> ^ w by A4, A7, A9;
then u = w by A1, Th6;
hence ( (R . 2) `2 = <%e%> ^ u or (R . 2) `2 = u ) by A5; :: thesis: verum

end;

suppose u1 in {(<%> E)} ; :: thesis: ( (R . 2) `2 = <%e%> ^ u or (R . 2) `2 = u )

then A10: u1 = <%> E by TARSKI:def 1;
( v = (R . 1) `2 & w = (R . 2) `2 ) by A4, A5;
hence ( (R . 2) `2 = <%e%> ^ u or (R . 2) `2 = u ) by A1, A7, A10; :: thesis: verum

end;

end;