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 A1: ( the carrier of TS1 = the carrier of TS2 & 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 Def6;
then ==>.-relation TS2 reduces [x1,x2],[y1,y2] by A1, Th34;
hence x1,x2 ==>* y1,y2,TS2 by Def6; :: thesis: verum