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))

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))

hence
not halt SCM+FSA in rng (Load (goto l))
; :: thesis: verumA1:
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;assume halt SCM+FSA in rng (Load (goto l)) ; :: thesis: contradiction

hence contradiction by A1, TARSKI:def 1; :: thesis: verum