let E be non empty set ; :: thesis: for F1, F2 being Subset of (E ^omega )
for TS1 being non empty transition-system of F1
for TS2 being non empty transition-system of 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 of F1
for TS2 being non empty transition-system of 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 of F1; :: thesis: for TS2 being non empty transition-system of 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 of 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 that
A1: the carrier of TS1 = the carrier of TS2 and
A2: 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
A3: len P > 0 ;

now

let i be Element of NAT ; :: thesis: ( i in dom P & i + 1 in dom P implies [(P . i),(P . (i + 1))] in ==>.-relation TS2 )
assume B: ( i in dom P & i + 1 in dom P ) ; :: thesis: [(P . i),(P . (i + 1))] in ==>.-relation TS2
[(P . i),(P . (i + 1))] in ==>.-relation TS1 by B, REWRITE1:def 2;
hence [(P . i),(P . (i + 1))] in ==>.-relation TS2 by A1, A2, ThRel20; :: thesis: verum

end;

hence P is RedSequence of ==>.-relation TS2 by A3, REWRITE1:def 2; :: thesis: verum