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 ==>.-relation TS reduces [x,w],[y,(v ^ w)] 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 ==>.-relation TS reduces [x,w],[y,(v ^ w)] 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 ==>.-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 over F st ==>.-relation TS reduces [x,w],[y,(v ^ w)] holds
v = <%> E
let TS be non empty transition-system over 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 Th75;
then (len v) + (len w) <= 0 + (len w) by AFINSQ_1:17;
hence v = <%> E by XREAL_1:6; :: thesis: verum