let E be non empty set ; :: 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 = u & (R . (len R)) `2 = <%> E holds
len R > len 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 = u & (R . (len R)) `2 = <%> E holds
len R > len u
let TS be non empty transition-system of (Lex E) \/ {(<%> E)}; :: thesis: for R being RedSequence of ==>.-relation TS st (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds
len R > len u
defpred S₁[ Nat] means for R being RedSequence of ==>.-relation TS
for u being Element of E ^omega st len R = $1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds
len R > len u;
A: S₁[ 0 ] ;

B: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: S₁[k] ; :: thesis: S₁[k + 1]

now

let R be RedSequence of ==>.-relation TS; :: thesis: for u being Element of E ^omega st len R = k + 1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds
len b₂ > len b₃
let u be Element of E ^omega ; :: thesis: ( len R = k + 1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E implies len b₁ > len b₂ )
assume C: ( len R = k + 1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E ) ; :: thesis: len b₁ > len b₂

per cases ( len u = 0 or len u > 0 ) ;

suppose len u = 0 ; :: thesis: len b₁ > len b₂

hence len R > len u ; :: thesis: verum

end;

suppose D2: len u > 0 ; :: thesis: len b₁ > len b₂

then consider e being Element of E, u1 being Element of E ^omega such that
D: u = <%e%> ^ u1 by ThTS3j;
len R <> 1 by C, D2;
then consider R' being RedSequence of ==>.-relation TS such that
E: ( <*(R . 1)*> ^ R' = R & (len R') + 1 = len R ) by REWRITE3:5, NAT_1:26;
I: (len R') + 0 < k + 1 by C, E, XREAL_1:8;
( rng R' <> {} & len R' >= 0 + 1 ) by NAT_1:8;
then K: ( 1 in dom R' & len R' in dom R' ) by FINSEQ_3:27;
then F: (<*(R . 1)*> ^ R') . (1 + 1) = R' . 1 by REWRITE3:1;
H: (R' . (len R')) `2 = <%> E by C, E, K, REWRITE3:1;

per cases ( (R . 2) `2 = <%e%> ^ u1 or (R . 2) `2 = u1 ) by C, D, ThTS3h;

suppose (R . 2) `2 = <%e%> ^ u1 ; :: thesis: len b₁ > len b₂

hence len R > len u by C, D, E, F, H, B1, I, XXREAL_0:2; :: thesis: verum

end;

suppose (R . 2) `2 = u1 ; :: thesis: len b₁ > len b₂

then len R' > len u1 by C, E, F, H, B1;
then len R > 1 + (len u1) by E, XREAL_1:8;
then len R > (len <%e%>) + (len u1) by AFINSQ_1:def 5;
hence len R > len u by D, AFINSQ_1:20; :: thesis: verum

end;

end;

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

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 & (R . (len R)) `2 = <%> E holds
len R > len u ; :: thesis: verum