let E be non empty set ; :: thesis: for u, v 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 = 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 of (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 of (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 );
A: S₁[ 0 ] ;

B: now

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume C: 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 D: ( len R = i + 1 & (R . 1) `2 = u ^ v & (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 len u = 0 ; :: thesis: ex l being Nat st
( l in dom R & (R . l) `2 = v )

then E: u = {} ;
set j = 1;
take 1 ; :: thesis: ( 1 in dom R & (R . 1) `2 = v )
rng R <> {} ;
hence 1 in dom R by FINSEQ_3:34; :: thesis: (R . 1) `2 = v
thus (R . 1) `2 = v by D, E, AFINSQ_1:32; :: thesis: verum

end;

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

then len u >= 0 + 1 by NAT_1:13;
then (len u) + (len v) >= 1 + (len v) by XREAL_1:8;
then len (u ^ v) >= 1 + (len v) by AFINSQ_1:20;
then len (u ^ v) >= 1 by LmNat1;
then (len R) + (len (u ^ v)) > (len (u ^ v)) + 1 by D, ThTS3g, XREAL_1:10;
then len R > 1 by XREAL_1:8;
then consider R' being RedSequence of ==>.-relation TS such that
F: ( (len R') + 1 = len R & ( for k being Nat st k in dom R' holds
R' . k = R . (k + 1) ) ) by REWRITE3:7;
G0: rng R' <> {} ;
then G1: 1 in dom R' by FINSEQ_3:34;
H: (R' . 1) `2 = (R . (1 + 1)) `2 by F, G0, FINSEQ_3:34;
1 <= len R' by G1, FINSEQ_3:27;
then len R' in dom R' by FINSEQ_3:27;
then H': (R' . (len R')) `2 = <%> E by D, F;
consider e being Element of E, u1 being Element of E ^omega such that
H2: u = <%e%> ^ u1 by D3, ThTS3j;
Z: (R . 1) `2 = <%e%> ^ (u1 ^ v) by D, H2, AFINSQ_1:30;
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 D, ThTS3h, Z;

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
I: ( l in dom R' & (R' . l) `2 = v ) by C, D, F, H, H';
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 I, F, ThTS3i; :: thesis: (R . (l + 1)) `2 = v
thus (R . (l + 1)) `2 = v by F, I; :: 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
I: ( l in dom R' & (R' . l) `2 = v ) by C, D, F, H, H';
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 I, F, ThTS3i; :: thesis: (R . (l + 1)) `2 = v
thus (R . (l + 1)) `2 = v by F, I; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A, B);
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