for k1 being Integer holds
( 0 in dom (Goto k1) & (Goto k1) . 0 = goto k1 ) by AFINSQ_1:65;