let x, y be set ; :: thesis: for E being non empty set
for u, w, v being Element of E ^omega
for TS being non empty transition-system of (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, w, v being Element of E ^omega
for TS being non empty transition-system of (Lex E) \/ {(<%> E)} st ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] holds
==>.-relation TS reduces [x,u],[y,v]
let u, w, v be Element of E ^omega ; :: thesis: for TS being non empty transition-system of (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 of (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 consider p being RedSequence of ==>.-relation TS such that
A: ( p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] ) by REWRITE1:def 3;
consider q being RedSequence of ==>.-relation TS such that
B: ( q . 1 = [x,u] & q . (len q) = [y,v] ) by A, ThTS3k'b;
thus ==>.-relation TS reduces [x,u],[y,v] by B, REWRITE1:def 3; :: thesis: verum