let x, y be set ; :: thesis: for E being non empty set
for u, v, w being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] holds
==>.-relation TS reduces [x,u],[y,v]
let E be non empty set ; :: thesis: for u, v, w being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] holds
==>.-relation TS reduces [x,u],[y,v]
let u, v, w be Element of E ^omega ; :: thesis: for TS being non empty transition-system over (Lex E) \/ {(<%> E)} st ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] holds
==>.-relation TS reduces [x,u],[y,v]
let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; :: thesis: ( ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] implies ==>.-relation TS reduces [x,u],[y,v] )
assume ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] ; :: thesis: ==>.-relation TS reduces [x,u],[y,v]
then ex p being RedSequence of ==>.-relation TS st
( p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] ) by REWRITE1:def 3;
then ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] ) by Th25;
hence ==>.-relation TS reduces [x,u],[y,v] by REWRITE1:def 3; :: thesis: verum