let E be non empty set ; :: thesis: for u 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 & (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 over (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 over (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;

A1: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

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

now :: thesis: for R being RedSequence of ==>.-relation TS
for u being Element of E ^omega st len R = k + 1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E holds
len R > len u

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 that
A3: len R = k + 1 and
A4: (R . 1) `2 = u and
A5: (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 A6: len u > 0 ; :: thesis: len b₁ > len b₂

then consider e being Element of E, u1 being Element of E ^omega such that
A7: u = <%e%> ^ u1 by Th7;
len R <> 1 by A4, A5, A6;
then consider R9 being RedSequence of ==>.-relation TS such that
A8: <*(R . 1)*> ^ R9 = R and
A9: (len R9) + 1 = len R by NAT_1:25, REWRITE3:5;
A10: (len R9) + 0 < k + 1 by A3, A9, XREAL_1:6;
A11: len R9 >= 0 + 1 by NAT_1:8;
then len R9 in dom R9 by FINSEQ_3:25;
then A12: (R9 . (len R9)) `2 = <%> E by A5, A8, A9, FINSEQ_3:103;
1 in dom R9 by A11, FINSEQ_3:25;
then A13: (<*(R . 1)*> ^ R9) . (1 + 1) = R9 . 1 by FINSEQ_3:103;

per cases ( (R . 2) `2 = <%e%> ^ u1 or (R . 2) `2 = u1 ) by A4, A5, A7, Th22;

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

hence len R > len u by A2, A3, A7, A8, A9, A10, A13, A12, XXREAL_0:2; :: thesis: verum

end;

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

then len R9 > len u1 by A2, A3, A8, A9, A13, A12;
then len R > 1 + (len u1) by A9, XREAL_1:6;
then len R > (len <%e%>) + (len u1) by AFINSQ_1:def 4;
hence len R > len u by A7, AFINSQ_1:17; :: thesis: verum

end;

end;

end;

end;

end;

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

end;

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