consider q1 being Element of tfsm such that
A1: q1 in qf by FINSEQ_4:87;
take the OFun of tfsm . [q1,s] ; :: thesis: ex q being State of tfsm st
( q in qf & the OFun of tfsm . [q1,s] = the OFun of tfsm . [q,s] )
thus ex q being State of tfsm st
( q in qf & the OFun of tfsm . [q1,s] = the OFun of tfsm . [q,s] ) by A1; :: thesis: verum