let l be Element of NAT ; :: thesis: ( dom (0 .--> (goto l)) = {0} & 0 in dom (0 .--> (goto l)) & (0 .--> (goto l)) . 0 = goto l & card (0 .--> (goto l)) = 1 & not halt SCM+FSA in rng (0 .--> (goto l)) )
thus dom (0 .--> (goto l)) = {0} by FUNCOP_1:13; :: thesis: ( 0 in dom (0 .--> (goto l)) & (0 .--> (goto l)) . 0 = goto l & card (0 .--> (goto l)) = 1 & not halt SCM+FSA in rng (0 .--> (goto l)) )
hence 0 in dom (0 .--> (goto l)) by TARSKI:def 1; :: thesis: ( (0 .--> (goto l)) . 0 = goto l & card (0 .--> (goto l)) = 1 & not halt SCM+FSA in rng (0 .--> (goto l)) )
thus (0 .--> (goto l)) . 0 = goto l by FUNCOP_1:72; :: thesis: ( card (0 .--> (goto l)) = 1 & not halt SCM+FSA in rng (0 .--> (goto l)) )
thus card (0 .--> (goto l)) = card <%(goto l)%> by AFINSQ_1:def 1
.= 1 by AFINSQ_1:34 ; :: thesis: not halt SCM+FSA in rng (0 .--> (goto l))

now

A1: rng (0 .--> (goto l)) = {(goto l)} by FUNCOP_1:8;
assume halt SCM+FSA in rng (0 .--> (goto l)) ; :: thesis: contradiction
hence contradiction by A1, TARSKI:def 1; :: thesis: verum

end;

hence not halt SCM+FSA in rng (0 .--> (goto l)) ; :: thesis: verum