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