let X be set ; 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 ; 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 ; 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)}; (w ^ v) -succ_of X,TS = v -succ_of (w -succ_of X,TS),TS
A1:
now let x be
set ;
( 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
;
x in (w ^ v) -succ_of X,TSthen 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;
verum end;
now let x be
set ;
( 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
;
x in v -succ_of (w -succ_of X,TS),TSthen 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;
verum end;
hence
(w ^ v) -succ_of X,TS = v -succ_of (w -succ_of X,TS),TS
by A1, TARSKI:2; verum