let x, y be object ; :: 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 non empty transition-system over F st x,w ==>* y,v ^ w,TS holds
v = <%> E
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 non empty transition-system over F st x,w ==>* y,v ^ w,TS holds
v = <%> E
let v, w be Element of E ^omega ; :: thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,w ==>* y,v ^ w,TS holds
v = <%> E
let F be Subset of (E ^omega); :: thesis: for TS being non empty transition-system over F st x,w ==>* y,v ^ w,TS holds
v = <%> E
let TS be non empty transition-system over F; :: thesis: ( x,w ==>* y,v ^ w,TS implies v = <%> E )
assume x,w ==>* y,v ^ w,TS ; :: thesis: v = <%> E
then len (v ^ w) <= len w by Th89;
then (len v) + (len w) <= 0 + (len w) by AFINSQ_1:17;
hence v = <%> E by XREAL_1:6; :: thesis: verum