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