rng (4 .--> (halt SCM)) = {(halt SCM)} by FUNCOP_1:14;
then B: halt SCM in rng (4 .--> (halt SCM)) by TARSKI:def 1;
rng (4 .--> (halt SCM)) c= rng ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) by FUNCT_4:19;
then C: halt SCM in rng ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) by B;
rng ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) c= rng ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) by FUNCT_4:19;
then D: halt SCM in rng ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) by C;
rng ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) c= rng ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) by FUNCT_4:19;
then A: halt SCM in rng ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) by D;
rng ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) c= rng Euclide-Algorithm by FUNCT_4:19;
hence halt SCM in rng Euclide-Algorithm by A; :: according to COMPOS_1:def 7 :: thesis: verum