( dom (3 .--> ((dl. 1) >0_goto 0)) = {3} & dom (4 .--> (halt SCM)) = {4} )
;
then A1: dom ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) =
{3} \/ {4}
by FUNCT_4:def 1
.=
{3,4}
by ENUMSET1:1
;
A2:
dom (1 .--> (Divide ((dl. 0),(dl. 1)))) = {1}
;
dom (2 .--> ((dl. 0) := (dl. 2))) = {2}
;
then dom ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) =
{2} \/ {3,4}
by A1, FUNCT_4:def 1
.=
{2,3,4}
by ENUMSET1:2
;
then A3: dom ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) =
{1} \/ {2,3,4}
by A2, FUNCT_4:def 1
.=
{1,2,3,4}
by ENUMSET1:4
;
dom (0 .--> ((dl. 2) := (dl. 1))) = {0}
;
then dom ((0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))))) =
{0} \/ {1,2,3,4}
by A3, FUNCT_4:def 1
.=
5
by CARD_1:53, ENUMSET1:7
;
hence
dom Euclid-Algorithm = 5
; verum