let x, y be object ; for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS )
let E be non empty set ; for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS )
let v, w be Element of E ^omega ; for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS )
let F be Subset of (E ^omega); for TS being non empty transition-system over F holds
( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS )
let TS be non empty transition-system over F; ( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS )
thus
( x,v -->. y,TS implies <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS )
( <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS implies x,v -->. y,TS )proof
assume
x,
v -->. y,
TS
;
<*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS
then
[[x,(v ^ w)],[y,w]] in ==>.-relation TS
by Th38;
hence
<*[x,(v ^ w)],[y,w]*> is
RedSequence of
==>.-relation TS
by REWRITE1:7;
verum
end;
assume
<*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS
; x,v -->. y,TS
then
[[x,(v ^ w)],[y,w]] in ==>.-relation TS
by Th8;
hence
x,v -->. y,TS
by Th38; verum