let l be Nat; :: thesis: ( dom (Load (goto l)) = {0} & 0 in dom (Load (goto l)) & (Load (goto l)) . 0 = goto l & card (Load (goto l)) = 1 & not halt SCM+FSA in rng (Load (goto l)) )
thus dom (Load (goto l)) = {0} by AFINSQ_1:def 4, CARD_1:49; :: thesis: ( 0 in dom (Load (goto l)) & (Load (goto l)) . 0 = goto l & card (Load (goto l)) = 1 & not halt SCM+FSA in rng (Load (goto l)) )
hence 0 in dom (Load (goto l)) by TARSKI:def 1; :: thesis: ( (Load (goto l)) . 0 = goto l & card (Load (goto l)) = 1 & not halt SCM+FSA in rng (Load (goto l)) )
thus (Load (goto l)) . 0 = goto l ; :: thesis: ( card (Load (goto l)) = 1 & not halt SCM+FSA in rng (Load (goto l)) )
thus card (Load (goto l)) = card <%(goto l)%>
.= 1 by AFINSQ_1:34 ; :: thesis: not halt SCM+FSA in rng (Load (goto l))
now :: thesis: not halt SCM+FSA in rng (Load (goto l))
A1: rng (Load (goto l)) = {(goto l)} by AFINSQ_1:33;
assume halt SCM+FSA in rng (Load (goto l)) ; :: thesis: contradiction
hence contradiction by A1, TARSKI:def 1; :: thesis: verum
end;
hence not halt SCM+FSA in rng (Load (goto l)) ; :: thesis: verum