let y be object ; :: thesis: for E being non empty set
for w 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 . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
let E be non empty set ; :: thesis: for w 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 . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
let w 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 . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
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 . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
let TS be non empty transition-system over F; :: thesis: for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
let P be RedSequence of ==>.-relation TS; :: thesis: ( P . (len P) = [y,w] implies for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w )
assume P . (len P) = [y,w] ; :: thesis: for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
then A1: (P . (len P)) `2 = {} ^ w
.= (<%> E) ^ w ;
defpred S₁[ Nat] means ( (len P) - $1 in dom P implies ex u being Element of E ^omega st (P . ((len P) - $1)) `2 = u ^ w );

A2: 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 A3: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: ( (len P) - (k + 1) in dom P implies ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w )

set len2 = (len P) - k;
set len1 = (len P) - (k + 1);
A4: ((len P) - (k + 1)) + 1 = (len P) - k ;
assume A5: (len P) - (k + 1) in dom P ; :: thesis: ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w
thus ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w :: thesis: verum

proof

per cases ( (len P) - k in dom P or not (len P) - k in dom P ) ;

suppose A6: (len P) - k in dom P ; :: thesis: ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w

then consider u1 being Element of E ^omega such that
A7: (P . ((len P) - k)) `2 = u1 ^ w by A3;
A8: [(P . ((len P) - (k + 1))),(P . ((len P) - k))] in ==>.-relation TS by A5, A4, A6, REWRITE1:def 2;
then consider x being Element of TS, v1 being Element of E ^omega , y being Element of TS, v2 being Element of E ^omega such that
A9: P . ((len P) - (k + 1)) = [x,v1] and
A10: P . ((len P) - k) = [y,v2] by Th31;
x,v1 ==>. y,v2,TS by A8, A9, A10, Def4;
then consider u2 being Element of E ^omega such that
x,u2 -->. y,TS and
A11: v1 = u2 ^ v2 ;
take u2 ^ u1 ; :: thesis: (P . ((len P) - (k + 1))) `2 = (u2 ^ u1) ^ w
(P . ((len P) - (k + 1))) `2 = u2 ^ v2 by A9, A11
.= u2 ^ (u1 ^ w) by A7, A10
.= (u2 ^ u1) ^ w by AFINSQ_1:27 ;
hence (P . ((len P) - (k + 1))) `2 = (u2 ^ u1) ^ w ; :: thesis: verum

end;

suppose not (len P) - k in dom P ; :: thesis: ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w

then (len P) - (k + 1) = (len P) - 0 by A5, A4, Th3;
hence ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w ; :: thesis: verum

end;

end;

end;

end;

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

end;

A12: S₁[ 0 ] by A1;
A13: for k being Nat holds S₁[k] from NAT_1:sch 2(A12, A2);

hereby :: thesis: verum

let k be Nat; :: thesis: ( k in dom P implies ex u being Element of E ^omega st (P . k) `2 = u ^ w )
assume A14: k in dom P ; :: thesis: ex u being Element of E ^omega st (P . k) `2 = u ^ w
k <= len P by A14, FINSEQ_3:25;
then consider l being Nat such that
A15: k + l = len P by NAT_1:10;
(k + l) - l = (len P) - l by A15;
hence ex u being Element of E ^omega st (P . k) `2 = u ^ w by A13, A14; :: thesis: verum

end;