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