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 ( 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 )
then A1: [(P . k),(P . (k + 1))] in ==>.-relation TS by 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
A2: ( P . k = [s,v] & P . (k + 1) = [t,w] ) by Th31;
A3: ( s in dom (dom the Tran of TS) & t in rng the Tran of TS ) by A1, A2, Th32;
A4: ( v in E ^omega & w in E ^omega ) ;
( s in TS & t in TS ) by A1, A2, Th32;
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 A2, A4, A3, MCART_1:7; :: thesis: verum