let x1, x2, y1, y2, z1, z2 be set ; :: thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system of F st x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS holds
x1,x2 ==>* z1,z2,TS
let E be non empty set ; :: thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system of F st x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS holds
x1,x2 ==>* z1,z2,TS
let F be Subset of (E ^omega); :: thesis: for TS being non empty transition-system of F st x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS holds
x1,x2 ==>* z1,z2,TS
let TS be non empty transition-system of F; :: thesis: ( x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS implies x1,x2 ==>* z1,z2,TS )
assume ( x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS ) ; :: thesis: x1,x2 ==>* z1,z2,TS
then ( ==>.-relation TS reduces [x1,x2],[y1,y2] & ==>.-relation TS reduces [y1,y2],[z1,z2] ) by Def6;
then ==>.-relation TS reduces [x1,x2],[z1,z2] by REWRITE1:17;
hence x1,x2 ==>* z1,z2,TS by Def6; :: thesis: verum