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 A1: ( q is accessible & q <> the InitS of S ) ; :: thesis: ex s being Element of I st q is_accessible_via s
then consider W being FinSequence of I such that
A2: the InitS of S,W -leads_to q by 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 A1, A2, FSM_1:def 3; :: thesis: verum

end;

then consider S being Element of I, w' being FinSequence of I such that
A3: ( W . 1 = S & W = <*S*> ^ w' ) by FINSEQ_3:111;
take S ; :: thesis: q is_accessible_via S
thus q is_accessible_via S by A2, A3, Def2; :: thesis: verum