( dom (3 .--> ((dl. 1) >0_goto 0 )) = {3} & dom (4 .--> (halt SCM )) = {4} )
by FUNCOP_1:19;
then A1: dom ((3 .--> ((dl. 1) >0_goto 0 )) +* (4 .--> (halt SCM ))) =
{3} \/ {4}
by FUNCT_4:def 1
.=
{3,4}
by ENUMSET1:41
;
A2:
dom (1 .--> (Divide (dl. 0 ),(dl. 1))) = {1}
by FUNCOP_1:19;
dom (2 .--> ((dl. 0 ) := (dl. 2))) = {2}
by FUNCOP_1:19;
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:42
;
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:44
;
dom (0 .--> ((dl. 2) := (dl. 1))) = {0 }
by FUNCOP_1:19;
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:91, ENUMSET1:47
;
hence
dom Euclide-Algorithm = 5
; verum