consider out being 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:] --> 1;
reconsider T = [:S,IAlph:] --> 1 as Function of [:S,IAlph:],S ;
reconsider OF = [:S,IAlph:] --> out as Function of [:S,IAlph:],OAlph ;
reconsider M = Mealy-FSM(# S,T,OF,IS #) as non empty finite Mealy-FSM of 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 Th17, TARSKI:def 1;
hence q is accessible by Def21; :: thesis: verum