let k1 be Integer; :: thesis: ( inspos 0 in dom ((inspos 0 ) .--> (goto k1)) & ((inspos 0 ) .--> (goto k1)) . (inspos 0 ) = goto k1 )
dom ((inspos 0 ) .--> (goto k1)) = {(inspos 0 )} by FUNCOP_1:19;
hence inspos 0 in dom ((inspos 0 ) .--> (goto k1)) by TARSKI:def 1; :: thesis: ((inspos 0 ) .--> (goto k1)) . (inspos 0 ) = goto k1
thus ((inspos 0 ) .--> (goto k1)) . (inspos 0 ) = goto k1 by FUNCOP_1:87; :: thesis: verum