let it1, it2 be Element of OAlph; :: thesis: ( ex q being State of tfsm st
( q in qf & it1 = the OFun of tfsm . [q,s] ) & ex q being State of tfsm st
( q in qf & it2 = the OFun of tfsm . [q,s] ) implies it1 = it2 )
given q1 being Element of tfsm such that A2: q1 in qf and
A3: it1 = the OFun of tfsm . [q1,s] ; :: thesis: ( for q being State of tfsm holds
( not q in qf or not it2 = the OFun of tfsm . [q,s] ) or it1 = it2 )
given q2 being Element of tfsm such that A4: q2 in qf and
A5: it2 = the OFun of tfsm . [q2,s] ; :: thesis: it1 = it2
final_states_partition tfsm is final by Def15;
then q1,q2 -are_equivalent by A2, A4;
hence it1 = it2 by A3, A5, Th19; :: thesis: verum