let E be non empty set ; :: thesis: for F being Subset of (E ^omega )
for TS being non empty transition-system of F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS )
let F be Subset of (E ^omega ); :: thesis: for TS being non empty transition-system of F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS )
let TS be non empty transition-system of F; :: thesis: for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P & k + 1 in dom P holds
( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS )
let P be RedSequence of ==>.-relation TS; :: thesis: for k being Nat st k in dom P & k + 1 in dom P holds
( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS )
let k be Nat; :: thesis: ( k in dom P & k + 1 in dom P implies ( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS ) )
assume A: ( k in dom P & k + 1 in dom P ) ; :: thesis: ( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS )
B: [(P . k),(P . (k + 1))] in ==>.-relation TS by A, REWRITE1:def 2;
then consider s being Element of TS, v being Element of E ^omega , t being Element of TS, w being Element of E ^omega such that
C: ( P . k = [s,v] & P . (k + 1) = [t,w] ) by ThRel10;
( s in TS & v in E ^omega & t in TS & w in E ^omega & s in dom (dom the Tran of TS) & t in rng the Tran of TS ) by B, C, ThRel11;
hence ( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS ) by C, MCART_1:7; :: thesis: verum