ex k being Element of NAT st ((Computation s) . k) `1 = the AcceptS of T by A1, Def9;
hence ex b<sub>1</sub> being All-State of T ex k being Element of NAT st
( b<sub>1</sub> = (Computation s) . k & ((Computation s) . k) `1 = the AcceptS of T ) ; :: thesis: verum