let I be non empty set ; :: thesis: for S being non empty FSM of I holds the InitS of S is accessible
let S be non empty FSM of 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 by FSM_1:def 3;
hence the InitS of S is accessible by Def3; :: thesis: verum