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 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 & (R . (len R)) `2 = <%> E holds
len R > len u;
A1: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; :: thesis: S1[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 b2 > len b3

let u be Element of E ^omega ; :: thesis: ( len R = k + 1 & (R . 1) `2 = u & (R . (len R)) `2 = <%> E implies len b1 > len b2 )
assume that
A3: len R = k + 1 and
A4: (R . 1) `2 = u and
A5: (R . (len R)) `2 = <%> E ; :: thesis: len b1 > len b2
per cases ( len u = 0 or len u > 0 ) ;
suppose len u = 0 ; :: thesis: len b1 > len b2
hence len R > len u ; :: thesis: verum
end;
suppose A6: len u > 0 ; :: thesis: len b1 > len b2
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 ;
A10: (len R9) + 0 < k + 1 by ;
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 ;
1 in dom R9 by ;
then A13: (<*(R . 1)*> ^ R9) . (1 + 1) = R9 . 1 by REWRITE3:1;
per cases ) `2 = <%e%> ^ u1 or (R . 2) `2 = u1 ) by A4, A5, A7, Th22;
suppose (R . 2) `2 = <%e%> ^ u1 ; :: thesis: len b1 > len b2
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 b1 > len b2
then len R9 > len u1 by A2, A3, A8, A9, A13, A12;
then len R > 1 + (len u1) by ;
then len R > () + (len u1) by AFINSQ_1:def 4;
hence len R > len u by ; :: thesis: verum
end;
end;
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A14: S1[ 0 ] ;
for k being Nat holds S1[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