let I be non empty set ; :: thesis: for s being Element of I
for S being non empty FSM of I
for q being State of S st q is_accessible_via s holds
q is accessible
let s be Element of I; :: thesis: for S being non empty FSM of I
for q being State of S st q is_accessible_via s holds
q is accessible
let S be non empty FSM of I; :: thesis: for q being State of S st q is_accessible_via s holds
q is accessible
let q be State of S; :: thesis: ( q is_accessible_via s implies q is accessible )
assume q is_accessible_via s ; :: thesis: q is accessible
then consider W being FinSequence of I such that
A1: the InitS of S,<*s*> ^ W -leads_to q by Def2;
take <*s*> ^ W ; :: according to FSM_2:def 3 :: thesis: the InitS of S,<*s*> ^ W -leads_to q
thus the InitS of S,<*s*> ^ W -leads_to q by A1; :: thesis: verum