set out = the Element of OAlph;
reconsider S = {1} as non empty finite set ;
reconsider IS = 1 as Element of S by TARSKI:def 1;
set dF = [:S,IAlph:];
set Tr = [:S,IAlph:] --> IS;
reconsider T = [:S,IAlph:] --> IS as Function of [:S,IAlph:],S ;
reconsider OF = [:S,IAlph:] --> the Element of OAlph as Function of [:S,IAlph:],OAlph ;
reconsider M = Mealy-FSM(# S,T,OF,IS #) as non empty finite Mealy-FSM over IAlph,OAlph ;
take M ; :: thesis: M is connected
let q be State of M; :: according to FSM_1:def 22 :: thesis: q is accessible
( q = 1 & the InitS of M, <*> IAlph -leads_to the InitS of M ) by Th2, TARSKI:def 1;
hence q is accessible ; :: thesis: verum