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 S<sub>1</sub>[ 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 S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A2: S₁[i] ; :: thesis: S₁[i + 1]
thus S₁[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 A7, NAT_1:13;
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 A4, A5, Th23, XREAL_1:8;
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 A10, FINSEQ_3:32;
1 in dom R9 by A11, FINSEQ_3:32;
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 A4, A8, AFINSQ_1:27;
thus ex k being Nat st
( k in dom R & (R . k) `2 = v ) :: thesis: verum

proof

per cases ( (R . 2) `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 A10, A15, A16; :: 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 A10, A17, A18; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

A19: S₁[ 0 ] ;
for k being Nat holds S₁[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