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:19; :: 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:87; :: thesis: ( card (0 .--> (goto l)) = 1 & not halt SCM+FSA in rng (0 .--> (goto l)) )
thus card (0 .--> (goto l)) = card (Load <*(goto l)*>) by SCMFSA7B:3
.= len <*(goto l)*> by SCMFSA_7:25
.= 1 by FINSEQ_1:56 ; :: thesis: not halt SCM+FSA in rng (0 .--> (goto l))

now

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

end;

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