let x1, x2, y1, y2 be set ; :: thesis: for E being non empty set
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 & x1,x2 ==>* y1,y2,TS1 holds
x1,x2 ==>* y1,y2,TS2
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 & x1,x2 ==>* y1,y2,TS1 holds
x1,x2 ==>* y1,y2,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 & x1,x2 ==>* y1,y2,TS1 holds
x1,x2 ==>* y1,y2,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 & x1,x2 ==>* y1,y2,TS1 holds
x1,x2 ==>* y1,y2,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 & x1,x2 ==>* y1,y2,TS1 implies x1,x2 ==>* y1,y2,TS2 )
assume that
A1: the carrier of TS1 = the carrier of TS2 and
A2: the Tran of TS1 = the Tran of TS2 ; :: thesis: ( not x1,x2 ==>* y1,y2,TS1 or x1,x2 ==>* y1,y2,TS2 )
assume x1,x2 ==>* y1,y2,TS1 ; :: thesis: x1,x2 ==>* y1,y2,TS2
then ==>.-relation TS1 reduces [x1,x2],[y1,y2] by DefTran;
then ==>.-relation TS2 reduces [x1,x2],[y1,y2] by A1, A2, ThRel20;
hence x1,x2 ==>* y1,y2,TS2 by DefTran; :: thesis: verum