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]] in ==>.-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]] in ==>.-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]] in ==>.-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]] in ==>.-relation TS )
let TS be non empty transition-system over F; ( x,v -->. y,TS iff [[x,(v ^ w)],[y,w]] in ==>.-relation TS )
thus
( x,v -->. y,TS implies [[x,(v ^ w)],[y,w]] in ==>.-relation TS )
( [[x,(v ^ w)],[y,w]] in ==>.-relation TS implies x,v -->. y,TS )proof
assume
x,
v -->. y,
TS
;
[[x,(v ^ w)],[y,w]] in ==>.-relation TS
then
x,
v ^ w ==>. y,
w,
TS
;
hence
[[x,(v ^ w)],[y,w]] in ==>.-relation TS
by Def4;
verum
end;
assume
[[x,(v ^ w)],[y,w]] in ==>.-relation TS
; x,v -->. y,TS
then
x,v ^ w ==>. y,w,TS
by Def4;
hence
x,v -->. y,TS
by Th24; verum