let x, y be set ; :: thesis: for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega )
for TS being transition-system of F holds
( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS )
let E be non empty set ; :: thesis: for v, w being Element of E ^omega
for F being Subset of (E ^omega )
for TS being transition-system of F holds
( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS )
let v, w be Element of E ^omega ; :: thesis: for F being Subset of (E ^omega )
for TS being transition-system of F holds
( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS )
let F be Subset of (E ^omega ); :: thesis: for TS being transition-system of F holds
( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS )
let TS be transition-system of F; :: thesis: ( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS )
thus ( x,v -->. y,TS implies x,v ^ w ==>. y,w,TS ) by DefDir; :: thesis: ( x,v ^ w ==>. y,w,TS implies x,v -->. y,TS )
assume x,v ^ w ==>. y,w,TS ; :: thesis: x,v -->. y,TS
then ex u being Element of E ^omega st
( x,u -->. y,TS & v ^ w = u ^ w ) by ThDir25;
hence x,v -->. y,TS by AFINSQ_1:31; :: thesis: verum