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