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 transition-system of F1
for TS2 being transition-system of F2 st 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 transition-system of F1
for TS2 being transition-system of F2 st 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 transition-system of F1
for TS2 being transition-system of F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds
x1,x2 ==>. y1,y2,TS2
let TS1 be transition-system of F1; :: thesis: for TS2 being transition-system of F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds
x1,x2 ==>. y1,y2,TS2
let TS2 be transition-system of F2; :: thesis: ( the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 implies x1,x2 ==>. y1,y2,TS2 )
assume that
A2: the Tran of TS1 = the Tran of TS2 and
A3: x1,x2 ==>. y1,y2,TS1 ; :: thesis: x1,x2 ==>. y1,y2,TS2
consider v, w being Element of E ^omega such that
B: ( v = y2 & x1,w -->. y1,TS1 & x2 = w ^ v ) by A3, DefDir;
take v ; :: according to REWRITE3:def 3 :: thesis: ex w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS2 & x2 = w ^ v )
take w ; :: thesis: ( v = y2 & x1,w -->. y1,TS2 & x2 = w ^ v )
thus ( v = y2 & x1,w -->. y1,TS2 & x2 = w ^ v ) by A2, B, ThProd40; :: thesis: verum