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 of (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 of (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 of (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 of (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 A: ( (R . 1) `2 = <%e%> ^ u & (R . (len R)) `2 = <%> E ) ; :: thesis: ( (R . 2) `2 = <%e%> ^ u or (R . 2) `2 = u )
A1: rng R <> {} ;
(R . 1) `2 <> (R . (len R)) `2 by A, AFINSQ_1:33;
then ( len R >= 1 + 1 & 2 >= 1 ) by NAT_1:8, NAT_1:26;
then 1 + 1 in dom R by FINSEQ_3:27;
then B: [(R . 1),(R . 2)] in ==>.-relation TS by A1, FINSEQ_3:34, REWRITE1:def 2;
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
C1: R . 1 = [p,v] and
C2: R . 2 = [q,w] by B, REWRITE3:31;
p,v ==>. q,w,TS by B, C1, C2, REWRITE3:def 4;
then consider u1 being Element of E ^omega such that
D: ( p,u1 -->. q,TS & v = u1 ^ w ) by REWRITE3:22;
E: u1 in (Lex E) \/ {(<%> E)} by D, REWRITE3:15;

per cases ( u1 in Lex E or u1 in {(<%> E)} ) by E, 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 ThLex20;
then consider f being Element of E such that
F: ( u1 = <%f%> & u1 . 0 = f ) by LmXSeq10;
(R . 1) `2 = <%f%> ^ w by C1, D, F, MCART_1:7;
then ( e = f & u = w ) by A, LmSeq30;
hence ( (R . 2) `2 = <%e%> ^ u or (R . 2) `2 = u ) by C2, MCART_1:7; :: thesis: verum

end;

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

then F: u1 = <%> E by TARSKI:def 1;
( v = (R . 1) `2 & w = (R . 2) `2 ) by C1, C2, MCART_1:7;
hence ( (R . 2) `2 = <%e%> ^ u or (R . 2) `2 = u ) by A, D, F, AFINSQ_1:32; :: thesis: verum

end;

end;