let X be set ; :: thesis: for E being non empty set
for w, v being Element of E ^omega
for TS being non empty transition-system of (Lex E) \/ {(<%> E)} holds (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS)
let E be non empty set ; :: thesis: for w, v being Element of E ^omega
for TS being non empty transition-system of (Lex E) \/ {(<%> E)} holds (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS)
let w, v be Element of E ^omega ; :: thesis: for TS being non empty transition-system of (Lex E) \/ {(<%> E)} holds (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS)
let TS be non empty transition-system of (Lex E) \/ {(<%> E)}; :: thesis: (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS)

A1: now

let x be set ; :: thesis: ( x in v -succ_of ((w -succ_of (X,TS)),TS) implies x in (w ^ v) -succ_of (X,TS) )
assume A2: x in v -succ_of ((w -succ_of (X,TS)),TS) ; :: thesis: x in (w ^ v) -succ_of (X,TS)
then reconsider r = x as Element of TS ;
consider p being Element of TS such that
A3: p in w -succ_of (X,TS) and
A4: p,v ==>* r,TS by A2, REWRITE3:103;
consider q being Element of TS such that
A5: q in X and
A6: q,w ==>* p,TS by A3, REWRITE3:103;
q,w ^ v ==>* r,TS by A4, A6, REWRITE3:99;
hence x in (w ^ v) -succ_of (X,TS) by A5, REWRITE3:103; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in (w ^ v) -succ_of (X,TS) implies x in v -succ_of ((w -succ_of (X,TS)),TS) )
assume A7: x in (w ^ v) -succ_of (X,TS) ; :: thesis: x in v -succ_of ((w -succ_of (X,TS)),TS)
then reconsider r = x as Element of TS ;
consider q being Element of TS such that
A8: q in X and
A9: q,w ^ v ==>* r,TS by A7, REWRITE3:103;
consider p being Element of TS such that
A10: q,w ==>* p,TS and
A11: p,v ==>* r,TS by A9, Th29;
p in w -succ_of (X,TS) by A8, A10, REWRITE3:103;
hence x in v -succ_of ((w -succ_of (X,TS)),TS) by A11, REWRITE3:103; :: thesis: verum

end;

hence (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS) by A1, TARSKI:1; :: thesis: verum