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

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