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 & 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 A3: ( q2 in qf & 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, A3, Def14;
hence it1 = it2 by A2, A3, Th36; :: thesis: verum