let k1 be Integer; :: thesis: ( 0 in dom (Goto k1) & (Goto k1) . 0 = goto k1 )
Goto k1 = 0 .--> (goto k1) by SCMPDS_4:def 1;
hence ( 0 in dom (Goto k1) & (Goto k1) . 0 = goto k1 ) by Lm1; :: thesis: verum