A1: dom (0 .--> ((dl. 2) := (dl. 1))) = {0 } by FUNCOP_1:19;
A2: dom (1 .--> (Divide (dl. 0 ),(dl. 1))) = {1} by FUNCOP_1:19;
A3: dom (2 .--> ((dl. 0 ) := (dl. 2))) = {2} by FUNCOP_1:19;
A4: dom (3 .--> ((dl. 1) >0_goto (il. 0 ))) = {3} by FUNCOP_1:19;
dom (4 .--> (halt SCM )) = {4} by FUNCOP_1:19;
then dom ((3 .--> ((dl. 1) >0_goto (il. 0 ))) +* (4 .--> (halt SCM ))) = {3} \/ {4} by A4, FUNCT_4:def 1
.= {3,4} by ENUMSET1:41 ;
then dom ((2 .--> ((dl. 0 ) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto (il. 0 ))) +* (4 .--> (halt SCM )))) = {2} \/ {3,4} by A3, FUNCT_4:def 1
.= {2,3,4} by ENUMSET1:42 ;
then dom ((1 .--> (Divide (dl. 0 ),(dl. 1))) +* ((2 .--> ((dl. 0 ) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto (il. 0 ))) +* (4 .--> (halt SCM ))))) = {1} \/ {2,3,4} by A2, FUNCT_4:def 1
.= {1,2,3,4} by ENUMSET1:44 ;
then dom ((0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide (dl. 0 ),(dl. 1))) +* ((2 .--> ((dl. 0 ) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto (il. 0 ))) +* (4 .--> (halt SCM )))))) = {0 } \/ {1,2,3,4} by A1, FUNCT_4:def 1
.= 5 by CARD_1:91, ENUMSET1:47 ;
hence dom Euclide-Algorithm = 5 ; :: thesis: verum