let X be set ; :: thesis: for E being non empty set
for w being Element of E ^omega
for F being Subset of ()
for TS being non empty transition-system over F
for S being Subset of TS st len w = 1 holds
( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let E be non empty set ; :: thesis: for w being Element of E ^omega
for F being Subset of ()
for TS being non empty transition-system over F
for S being Subset of TS st len w = 1 holds
( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let w be Element of E ^omega ; :: thesis: for F being Subset of ()
for TS being non empty transition-system over F
for S being Subset of TS st len w = 1 holds
( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let F be Subset of (); :: thesis: for TS being non empty transition-system over F
for S being Subset of TS st len w = 1 holds
( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let TS be non empty transition-system over F; :: thesis: for S being Subset of TS st len w = 1 holds
( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let S be Subset of TS; :: thesis: ( len w = 1 implies ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS ) )
assume A1: len w = 1 ; :: thesis: ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )
thus ( X = w -succ_of (S,TS) implies S,w ==>* X, _bool TS ) :: thesis: ( S,w ==>* X, _bool TS implies X = w -succ_of (S,TS) )
proof
assume X = w -succ_of (S,TS) ; :: thesis: S,w ==>* X, _bool TS
then [[S,w],X] in the Tran of (_bool TS) by ;
then S,w -->. X, _bool TS by REWRITE3:def 2;
then S,w ==>. X, <%> E, _bool TS by REWRITE3:23;
then S,w ==>* X, <%> E, _bool TS by REWRITE3:87;
hence S,w ==>* X, _bool TS by REWRITE3:def 7; :: thesis: verum
end;
assume S,w ==>* X, _bool TS ; :: thesis: X = w -succ_of (S,TS)
then A2: S,w ==>* X, <%> E, _bool TS by REWRITE3:def 7;
ex e being Element of E st
( w = <%e%> & w . 0 = e ) by ;
then S,w ^ {} ==>. X, <%> E, _bool TS by ;
then A3: S,w -->. X, _bool TS by REWRITE3:24;
then X in _bool TS by REWRITE3:15;
then X in the carrier of (_bool TS) ;
then reconsider X9 = X as Subset of TS by Def1;
[[S,w],X9] in the Tran of (_bool TS) by ;
hence X = w -succ_of (S,TS) by Def1; :: thesis: verum