let x, y be set ; :: thesis: for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega )
for TS being non empty transition-system of F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
let E be non empty set ; :: thesis: for u being Element of E ^omega
for F being Subset of (E ^omega )
for TS being non empty transition-system of F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
let u be Element of E ^omega ; :: thesis: for F being Subset of (E ^omega )
for TS being non empty transition-system of F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
let F be Subset of (E ^omega ); :: thesis: for TS being non empty transition-system of F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
let TS be non empty transition-system of F; :: thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1 )
assume A: not <%> E in rng (dom the Tran of TS) ; :: thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
defpred S₁[ Nat] means for P being RedSequence of ==>.-relation TS
for u being Element of E ^omega
for x being set st len u = $1 & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1;

C: now

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume C1: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]

now

let P be RedSequence of ==>.-relation TS; :: thesis: for u being Element of E ^omega
for x being set st len u = k & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len b₃ <= (len b₄) + 1
let u be Element of E ^omega ; :: thesis: for x being set st len u = k & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len b₂ <= (len b₃) + 1
let x be set ; :: thesis: ( len u = k & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] implies len b₁ <= (len b₂) + 1 )
assume C2: ( len u = k & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] ) ; :: thesis: len b₁ <= (len b₂) + 1

per cases ( len u < 1 or len u >= 1 ) ;

suppose len u < 1 ; :: thesis: len b₁ <= (len b₂) + 1

then u = <%> E by NAT_1:26;
then len P = 1 by A, C2, ThRedSeq80;
hence len P <= (len u) + 1 by NAT_1:26; :: thesis: verum

end;

suppose C3: len u >= 1 ; :: thesis: len b₁ <= (len b₂) + 1

C4': len P <> 1

proof

assume len P = 1 ; :: thesis: contradiction
then u = <%> E by C2, ZFMISC_1:33;
hence contradiction by C3; :: thesis: verum

end;

then C5: len P > 1 by NAT_1:26;
consider P' being RedSequence of ==>.-relation TS such that
D: ( <*(P . 1)*> ^ P' = P & (len P') + 1 = len P ) by C4', LmRed10, NAT_1:26;
( len P >= 1 & len P >= 1 + 1 ) by C5, NAT_1:13;
then D2: ( 1 in dom P & 1 + 1 in dom P ) by FINSEQ_3:27;
then D3: P . (1 + 1) = [((P . (1 + 1)) `1 ),((P . (1 + 1)) `2 )] by ThRedSeq5;
then D4: [[x,u],[((P . (1 + 1)) `1 ),((P . (1 + 1)) `2 )]] in ==>.-relation TS by C2, D2, REWRITE1:def 2;
then reconsider u1 = (P . (1 + 1)) `2 as Element of E ^omega by ThRel11;
x,u ==>. (P . (1 + 1)) `1 ,u1,TS by D4, DefRel;
then consider v being Element of E ^omega such that
D5: ( x,v -->. (P . (1 + 1)) `1 ,TS & u = v ^ u1 ) by ThDir25;
D6: v <> <%> E by A, D5, ThProd30;
len u = (len u1) + (len v) by D5, AFINSQ_1:20;
then E0: (len u) - 0 > ((len u1) + (len v)) - (len v) by D6, XREAL_1:17;
E2: len <*(P . 1)*> = 1 by FINSEQ_1:56;
E3: len P' >= 1 by NAT_1:26;
E4: P' . 1 = [((P . (1 + 1)) `1 ),u1] by D, D3, E2, E3, FINSEQ_1:86;
P' . (len P') = [y,(<%> E)] by C2, D, E2, E3, FINSEQ_1:86;
then F: len P' <= (len u1) + 1 by E0, E4, C1, C2;
(len u1) + 1 <= len u by E0, NAT_1:13;
then len P' <= len u by F, XXREAL_0:2;
hence len P <= (len u) + 1 by D, XREAL_1:8; :: thesis: verum

end;

end;

end;

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

end;

for k being Nat holds S₁[k] from NAT_1:sch 4(C);
hence for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1 ; :: thesis: verum