for IAlph, OAlph being non empty set
for w being FinSequence of IAlph
for tfsm, rtfsm being non empty finite Mealy-FSM over IAlph,OAlph
for q being State of tfsm
for qr being State of rtfsm st rtfsm = the_reduction_of tfsm & q in qr holds
for k being Nat st k in Seg ((len w) + 1) holds
((q,w) -admissible) . k in ((qr,w) -admissible) . k