let X be set ; :: thesis: for E being non empty set

for v, w being Element of E ^omega

for TS being non empty transition-system over (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 v, w being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS)

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

for v, w being Element of E ^omega

for TS being non empty transition-system over (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 v, w being Element of E ^omega

for TS being non empty transition-system over (Lex E) \/ {(<%> E)} holds (w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS)

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

A1: now :: thesis: for x being object st x in v -succ_of ((w -succ_of (X,TS)),TS) holds

x in (w ^ v) -succ_of (X,TS)

x in (w ^ v) -succ_of (X,TS)

let x be object ; :: 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;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

now :: thesis: for x being object st x in (w ^ v) -succ_of (X,TS) holds

x in v -succ_of ((w -succ_of (X,TS)),TS)

hence
(w ^ v) -succ_of (X,TS) = v -succ_of ((w -succ_of (X,TS)),TS)
by A1, TARSKI:2; :: thesis: verumx in v -succ_of ((w -succ_of (X,TS)),TS)

let x be object ; :: 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, Th28;

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;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, Th28;

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