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
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u
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
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u
let u be Element of E ^omega ; :: thesis: for F being Subset of (E ^omega )
for TS being non empty transition-system of F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u
let F be Subset of (E ^omega ); :: thesis: for TS being non empty transition-system of F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u
let TS be non empty transition-system of F; :: thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u
defpred S<sub>1</sub>[ Nat] means for P being RedSequence of ==>.-relation TS
for x, y being set st P . 1 = [x,u] & P . (len P) = [y,u] & len P = $1 holds
for k being Nat st k in dom P holds
(P . k) `2 = u;
C: S₁[ 0 ] ;

D: now

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

now

let P be RedSequence of ==>.-relation TS; :: thesis: for x, y being set st P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 holds
for l being Nat st b₆ in dom l holds
(l . b₆) `2 = u
let x, y be set ; :: thesis: ( P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 implies for l being Nat st b<sub>4</sub> in dom l holds
(l . b<sub>4</sub>) `2 = u )
assume that
D1: ( P . 1 = [x,u] & P . (len P) = [y,u] ) and
D2: len P = k + 1 ; :: thesis: for l being Nat st b₄ in dom l holds
(l . b₄) `2 = u

per cases ( k = 0 or k <> 0 ) ;

suppose D3: k = 0 ; :: thesis: for l being Nat st b₄ in dom l holds
(l . b₄) `2 = u

hereby :: thesis: verum

let l be Nat; :: thesis: ( l in dom P implies (P . l) `2 = u )
assume l in dom P ; :: thesis: (P . l) `2 = u
then ( l <= 1 & 1 <= l ) by D2, D3, FINSEQ_3:27;
then l = 1 by XXREAL_0:1;
hence (P . l) `2 = u by D1, MCART_1:7; :: thesis: verum

end;

end;

suppose k <> 0 ; :: thesis: for l being Nat st b₄ in dom l holds
(l . b₄) `2 = u

then D2'A: k + 1 > 0 + 1 by XREAL_1:8;
then consider Q being RedSequence of ==>.-relation TS such that
D3: ( <*(P . 1)*> ^ Q = P & len P = (len Q) + 1 ) by D2, LmRed10;
D2': len <*(P . 1)*> = 1 by FINSEQ_1:57;
D6': len Q >= 0 + 1 by NAT_1:8;
then D6: Q . (len Q) = [y,u] by D1, D2', D3, FINSEQ_1:86;
len P >= 1 + 1 by D2, D2'A, NAT_1:8;
then D6'A: ( 1 in dom P & 1 + 1 in dom P ) by D2, D2'A, FINSEQ_3:27;
then D6'C: P . (1 + 1) = [((P . (1 + 1)) `1 ),((P . (1 + 1)) `2 )] by ThRedSeq5;
then D6'B: Q . 1 = [((P . (1 + 1)) `1 ),((P . (1 + 1)) `2 )] by D2', D3, D6', FINSEQ_1:86;
reconsider u1 = (P . (1 + 1)) `2 as Element of E ^omega by D6'A, ThRedSeq10;
consider v being Element of E ^omega such that
E1: u1 = v ^ u by D6, D6'B, ThRedSeq60;
==>.-relation TS reduces P . 1,P . (1 + 1) by D6'A, REWRITE1:18;
then consider P' being RedSequence of ==>.-relation TS such that
E1': ( P' . 1 = P . 1 & P' . (len P') = P . (1 + 1) ) by REWRITE1:def 3;
consider w being Element of E ^omega such that
E2: u = w ^ u1 by D1, D6'C, E1', ThRedSeq60;
u = (w ^ v) ^ u by E1, E2, AFINSQ_1:30;
then w ^ v = {} by FLANG_2:4;
then w = {} by AFINSQ_1:33;
then D5: Q . 1 = [((P . (1 + 1)) `1 ),u] by D6'B, E2, AFINSQ_1:32;

hereby :: thesis: verum

let l be Nat; :: thesis: ( l in dom P implies (P . b₁) `2 = u )
assume l in dom P ; :: thesis: (P . b<sub>1</sub>) `2 = u
then D7'A: ( 1 <= l & l <= len P ) by FINSEQ_3:27;
then ( 1 + 1 <= l + 1 & l <= len P ) by XREAL_1:8;
then ( ( 1 + 1 = l + 1 or 1 + 1 <= l ) & l <= len P ) by NAT_1:8;
then D7': ( 1 = l or ( (1 + 1) - 1 <= l - 1 & l - 1 <= ((len Q) + 1) - 1 ) ) by D3, XREAL_1:11;
reconsider l' = l - 1 as Element of NAT by D7'A, NAT_1:21;
D7: ( l = 1 or l' in dom Q ) by D7', FINSEQ_3:27;

per cases ( l = 1 or l - 1 in dom Q ) by D7;

suppose l = 1 ; :: thesis: (P . b₁) `2 = u

hence (P . l) `2 = u by D1, MCART_1:7; :: thesis: verum

end;

suppose D8: l - 1 in dom Q ; :: thesis: (P . b₁) `2 = u

then D9: (Q . (l - 1)) `2 = u by D0, D2, D3, D5, D6;
( 1 <= l - 1 & l - 1 <= len Q ) by D8, FINSEQ_3:27;
then ( 1 + 0 < (l - 1) + 1 & (l - 1) + 1 <= (len Q) + 1 ) by XREAL_1:8;
hence (P . l) `2 = u by D2', D3, D9, FINSEQ_1:37; :: thesis: verum

end;

end;

end;

end;

end;

end;

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

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(C, D);
hence for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u ; :: thesis: verum