let k1 be Integer; :: thesis: ( 0 in dom (Goto k1) & (Goto k1) . 0 = goto k1 )
Goto k1 = <%(goto k1)%> by SCMPDS_4:def 1;
hence ( 0 in dom (Goto k1) & (Goto k1) . 0 = goto k1 ) by AFINSQ_1:38, AFINSQ_1:69; :: thesis: verum