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