let x, y be object ; :: 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 over 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 over 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 over 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 over 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 over 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 object 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;

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 P being RedSequence of ==>.-relation TS
for x, y being object st P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 holds
for l being Nat st l in dom P holds
(P . l) `2 = u

let P be RedSequence of ==>.-relation TS; :: thesis: for x, y being object 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 object ; :: 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
A3: P . 1 = [x,u] and
A4: P . (len P) = [y,u] and
A5: 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 A6: 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 A5, A6, FINSEQ_3:25;
then l = 1 by XXREAL_0:1;
hence (P . l) `2 = u by A3; :: thesis: verum

end;

end;

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

then A7: k + 1 > 0 + 1 by XREAL_1:6;
then A8: 1 in dom P by A5, FINSEQ_3:25;
len P >= 1 + 1 by A5, A7, NAT_1:8;
then A9: 1 + 1 in dom P by FINSEQ_3:25;
then A10: P . (1 + 1) = [((P . (1 + 1)) `1),((P . (1 + 1)) `2)] by A8, Th48;
reconsider u1 = (P . (1 + 1)) `2 as Element of E ^omega by A8, A9, Th49;
==>.-relation TS reduces P . 1,P . (1 + 1) by A8, A9, REWRITE1:17;
then ex P9 being RedSequence of ==>.-relation TS st
( P9 . 1 = P . 1 & P9 . (len P9) = P . (1 + 1) ) by REWRITE1:def 3;
then consider w being Element of E ^omega such that
A11: u = w ^ u1 by A3, A10, Th53;
A12: len <*(P . 1)*> = 1 by FINSEQ_1:40;
consider Q being RedSequence of ==>.-relation TS such that
A13: <*(P . 1)*> ^ Q = P and
A14: len P = (len Q) + 1 by A5, A7, Th5;
A15: len Q >= 0 + 1 by NAT_1:8;
then A16: Q . 1 = [((P . (1 + 1)) `1),((P . (1 + 1)) `2)] by A13, A12, A10, FINSEQ_1:65;
A17: Q . (len Q) = [y,u] by A4, A13, A14, A12, A15, FINSEQ_1:65;
then consider v being Element of E ^omega such that
A18: u1 = v ^ u by A16, Th53;
A19: {} ^ u1 = u1 ;
u = (w ^ v) ^ u by A18, A11, AFINSQ_1:27;
then w ^ v = {} by FLANG_2:4;
then A20: Q . 1 = [((P . (1 + 1)) `1),u] by A16, A11, A19, AFINSQ_1:30;

hereby :: thesis: verum

let l be Nat; :: thesis: ( l in dom P implies (P . b₁) `2 = u )
assume A21: l in dom P ; :: thesis: (P . b<sub>1</sub>) `2 = u
then A22: 1 <= l by FINSEQ_3:25;
then reconsider l9 = l - 1 as Nat by NAT_1:21;
1 + 1 <= l + 1 by A22, XREAL_1:6;
then A23: ( 1 + 1 = l + 1 or 1 + 1 <= l ) by NAT_1:8;
l <= len P by A21, FINSEQ_3:25;
then ( 1 = l or ( (1 + 1) - 1 <= l - 1 & l - 1 <= ((len Q) + 1) - 1 ) ) by A14, A23, XREAL_1:9;
then A24: ( l = 1 or l9 in dom Q ) by FINSEQ_3:25;

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

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

hence (P . l) `2 = u by A3; :: thesis: verum

end;

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

then l - 1 <= len Q by FINSEQ_3:25;
then A26: (l - 1) + 1 <= (len Q) + 1 by XREAL_1:6;
1 <= l - 1 by A25, FINSEQ_3:25;
then A27: 1 + 0 < (l - 1) + 1 by XREAL_1:6;
(Q . (l - 1)) `2 = u by A2, A5, A14, A17, A20, A25;
hence (P . l) `2 = u by A13, A14, A12, A27, A26, FINSEQ_1:24; :: thesis: verum

end;

end;

end;

end;

end;

end;

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

end;

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