let E be non empty set ; :: thesis: for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds
for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2
let F1, F2 be Subset of (E ^omega); :: thesis: for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds
for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2
let TS1 be non empty transition-system over F1; :: thesis: for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds
for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2
let TS2 be non empty transition-system over F2; :: thesis: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 implies for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2 )
assume A1: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 ) ; :: thesis: for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2
let P be RedSequence of ==>.-relation TS1; :: thesis: P is RedSequence of ==>.-relation TS2
A2: now :: thesis: for i being Nat st i in dom P & i + 1 in dom P holds
[(P . i),(P . (i + 1))] in ==>.-relation TS2
let i be Nat; :: thesis: ( i in dom P & i + 1 in dom P implies [(P . i),(P . (i + 1))] in ==>.-relation TS2 )
assume ( i in dom P & i + 1 in dom P ) ; :: thesis: [(P . i),(P . (i + 1))] in ==>.-relation TS2
then [(P . i),(P . (i + 1))] in ==>.-relation TS1 by REWRITE1:def 2;
hence [(P . i),(P . (i + 1))] in ==>.-relation TS2 by A1, Th34; :: thesis: verum
end;
len P > 0 ;
hence P is RedSequence of ==>.-relation TS2 by A2, REWRITE1:def 2; :: thesis: verum