let E be non empty set ; :: thesis: for u, v 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 = u ^ v & (R . (len R)) `2 = <%> E holds
ex l being Nat st
( l in dom R & (R . l) `2 = v )

let u, v 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 = u ^ v & (R . (len R)) `2 = <%> E holds
ex l being Nat st
( l in dom R & (R . l) `2 = v )

let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; :: thesis: for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds
ex l being Nat st
( l in dom R & (R . l) `2 = v )

defpred S1[ Nat] means for R being RedSequence of ==>.-relation TS
for u being Element of E ^omega st len R = \$1 & (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds
ex l being Nat st
( l in dom R & (R . l) `2 = v );
A1: now :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A2: S1[i] ; :: thesis: S1[i + 1]
thus S1[i + 1] :: thesis: verum
proof
let R be RedSequence of ==>.-relation TS; :: thesis: for u being Element of E ^omega st len R = i + 1 & (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds
ex l being Nat st
( l in dom R & (R . l) `2 = v )

let u be Element of E ^omega ; :: thesis: ( len R = i + 1 & (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E implies ex l being Nat st
( l in dom R & (R . l) `2 = v ) )

assume that
A3: len R = i + 1 and
A4: (R . 1) `2 = u ^ v and
A5: (R . (len R)) `2 = <%> E ; :: thesis: ex l being Nat st
( l in dom R & (R . l) `2 = v )

per cases ( len u = 0 or len u > 0 ) ;
suppose A6: len u = 0 ; :: thesis: ex l being Nat st
( l in dom R & (R . l) `2 = v )

set j = 1;
take 1 ; :: thesis: ( 1 in dom R & (R . 1) `2 = v )
rng R <> {} ;
hence 1 in dom R by FINSEQ_3:32; :: thesis: (R . 1) `2 = v
u = {} by A6;
hence (R . 1) `2 = v by A4; :: thesis: verum
end;
suppose A7: len u > 0 ; :: thesis: ex l being Nat st
( l in dom R & (R . l) `2 = v )

then consider e being Element of E, u1 being Element of E ^omega such that
A8: u = <%e%> ^ u1 by Th7;
len u >= 0 + 1 by ;
then (len u) + (len v) >= 1 + (len v) by XREAL_1:6;
then len (u ^ v) >= 1 + (len v) by AFINSQ_1:17;
then len (u ^ v) >= 1 by Th1;
then (len R) + (len (u ^ v)) > (len (u ^ v)) + 1 by ;
then len R > 1 by XREAL_1:6;
then consider R9 being RedSequence of ==>.-relation TS such that
A9: (len R9) + 1 = len R and
A10: for k being Nat st k in dom R9 holds
R9 . k = R . (k + 1) by REWRITE3:7;
A11: rng R9 <> {} ;
then A12: (R9 . 1) `2 = (R . (1 + 1)) `2 by ;
1 in dom R9 by ;
then 1 <= len R9 by FINSEQ_3:25;
then len R9 in dom R9 by FINSEQ_3:25;
then A13: (R9 . (len R9)) `2 = <%> E by A5, A9, A10;
A14: (R . 1) `2 = <%e%> ^ (u1 ^ v) by ;
thus ex k being Nat st
( k in dom R & (R . k) `2 = v ) :: thesis: verum
proof
per cases ) `2 = u ^ v or (R . 2) `2 = u1 ^ v ) by A4, A5, A14, Th22;
suppose (R . 2) `2 = u ^ v ; :: thesis: ex k being Nat st
( k in dom R & (R . k) `2 = v )

then consider l being Nat such that
A15: l in dom R9 and
A16: (R9 . l) `2 = v by A2, A3, A9, A12, A13;
set k = l + 1;
take l + 1 ; :: thesis: ( l + 1 in dom R & (R . (l + 1)) `2 = v )
thus l + 1 in dom R by A9, A15, Th3; :: thesis: (R . (l + 1)) `2 = v
thus (R . (l + 1)) `2 = v by ; :: thesis: verum
end;
suppose (R . 2) `2 = u1 ^ v ; :: thesis: ex k being Nat st
( k in dom R & (R . k) `2 = v )

then consider l being Nat such that
A17: l in dom R9 and
A18: (R9 . l) `2 = v by A2, A3, A9, A12, A13;
set k = l + 1;
take l + 1 ; :: thesis: ( l + 1 in dom R & (R . (l + 1)) `2 = v )
thus l + 1 in dom R by A9, A17, Th3; :: thesis: (R . (l + 1)) `2 = v
thus (R . (l + 1)) `2 = v by ; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
A19: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A19, A1);
hence for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u ^ v & (R . (len R)) `2 = <%> E holds
ex l being Nat st
( l in dom R & (R . l) `2 = v ) ; :: thesis: verum