let I be non empty set ; :: thesis: for S being non empty FSM over I holds the InitS of S is accessible
let S be non empty FSM over I; :: thesis: the InitS of S is accessible
set w = <*> I;
(GEN ((<*> I), the InitS of S)) . ((len (<*> I)) + 1) = the InitS of S by FSM_1:def 2;
then the InitS of S, <*> I -leads_to the InitS of S ;
hence the InitS of S is accessible ; :: thesis: verum