ex k being Element of NAT st ((Computation s) . k) `1_3 = the AcceptS of T by A1, Def8;
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_3 = the AcceptS of T ) ; :: thesis: verum