let I be non empty set ; :: thesis: for S being non empty FSM of 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 of 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, Def3;
W <> {}

proof

assume W = {} ; :: thesis: contradiction
then len W = 0 ;
then (GEN (W, the InitS of S)) . ((len W) + 1) = the InitS of S by FSM_1:def 2;
hence contradiction by A2, A3, FSM_1:def 3; :: thesis: verum

end;

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, Def2; :: thesis: verum