let y be set ; :: 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 of 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 of 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 of 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 of 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 of 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 A: 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
defpred S<sub>1</sub>[ Nat] means ( (len P) - $1 in dom P implies ex u being Element of E ^omega st (P . ((len P) - $1)) `2 = u ^ w );
B: S₁[ 0 ]

proof

(P . (len P)) `2 = w by A, MCART_1:7;
then (P . (len P)) `2 = (<%> E) ^ w by AFINSQ_1:32;
hence S₁[ 0 ] ; :: thesis: verum

end;

C: now

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

now

assume C1: (len P) - (k + 1) in dom P ; :: thesis: ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w
set len1 = (len P) - (k + 1);
set len2 = (len P) - k;
C2: ((len P) - (k + 1)) + 1 = (len P) - k ;
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 D0: (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
D2: (P . ((len P) - k)) `2 = u1 ^ w by C0;
D3: [(P . ((len P) - (k + 1))),(P . ((len P) - k))] in ==>.-relation TS by C1, C2, D0, 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
D4: ( P . ((len P) - (k + 1)) = [x,v1] & P . ((len P) - k) = [y,v2] ) by ThRel10;
x,v1 ==>. y,v2,TS by D3, D4, DefRel;
then consider u2 being Element of E ^omega such that
D5: ( x,u2 -->. y,TS & v1 = u2 ^ v2 ) by ThDir25;
D6: (P . ((len P) - (k + 1))) `2 = u2 ^ v2 by D4, D5, MCART_1:7
.= u2 ^ (u1 ^ w) by D2, D4, MCART_1:7
.= (u2 ^ u1) ^ w by AFINSQ_1:30 ;
take u2 ^ u1 ; :: thesis: (P . ((len P) - (k + 1))) `2 = (u2 ^ u1) ^ w
thus (P . ((len P) - (k + 1))) `2 = (u2 ^ u1) ^ w by D6; :: 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 C1, C2, LmSeq40;
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;

E: for k being Nat holds S₁[k] from NAT_1:sch 2(B, C);

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 F0: k in dom P ; :: thesis: ex u being Element of E ^omega st (P . k) `2 = u ^ w
k <= len P by F0, FINSEQ_3:27;
then consider l being Nat such that
F1: k + l = len P by NAT_1:10;
(k + l) - l = (len P) - l by F1;
hence ex u being Element of E ^omega st (P . k) `2 = u ^ w by F0, E; :: thesis: verum

end;