let I be non empty set ; :: thesis: for S being non empty FSM over I

for q being State of S st q is accessible & q <> the InitS of S holds

ex s being Element of I st q is_accessible_via s

let S be non empty FSM over I; :: thesis: for q being State of S st q is accessible & q <> the InitS of S holds

ex s being Element of I st q is_accessible_via s

let q be State of S; :: thesis: ( q is accessible & q <> the InitS of S implies ex s being Element of I st q is_accessible_via s )

assume that

A1: q is accessible and

A2: q <> the InitS of S ; :: thesis: ex s being Element of I st q is_accessible_via s

consider W being FinSequence of I such that

A3: the InitS of S,W -leads_to q by A1;

W <> {} by FSM_1:def 2, A2, A3;

then consider S being Element of I, w9 being FinSequence of I such that

W . 1 = S and

A4: W = <*S*> ^ w9 by FINSEQ_3:102;

take S ; :: thesis: q is_accessible_via S

thus q is_accessible_via S by A3, A4; :: thesis: verum

for q being State of S st q is accessible & q <> the InitS of S holds

ex s being Element of I st q is_accessible_via s

let S be non empty FSM over I; :: thesis: for q being State of S st q is accessible & q <> the InitS of S holds

ex s being Element of I st q is_accessible_via s

let q be State of S; :: thesis: ( q is accessible & q <> the InitS of S implies ex s being Element of I st q is_accessible_via s )

assume that

A1: q is accessible and

A2: q <> the InitS of S ; :: thesis: ex s being Element of I st q is_accessible_via s

consider W being FinSequence of I such that

A3: the InitS of S,W -leads_to q by A1;

W <> {} by FSM_1:def 2, A2, A3;

then consider S being Element of I, w9 being FinSequence of I such that

W . 1 = S and

A4: W = <*S*> ^ w9 by FINSEQ_3:102;

take S ; :: thesis: q is_accessible_via S

thus q is_accessible_via S by A3, A4; :: thesis: verum