per cases ( i in dom p or not i in dom p ) ;

suppose i in dom p ; :: thesis: Replace (p,i,a) is D -valued

then Replace (p,i,a) = p +* (i .--> a) by FUNCT_7:def 3;
then A1: rng (Replace (p,i,a)) c= (rng p) \/ (rng (i .--> a)) by FUNCT_4:17;
rng (i .--> a) = {a} by FUNCOP_1:8;
then A2: rng (i .--> a) c= D by ZFMISC_1:31;
rng p c= D by RELAT_1:def 19;
then (rng p) \/ (rng (i .--> a)) c= D by A2, XBOOLE_1:8;
hence rng (Replace (p,i,a)) c= D by A1; :: according to RELAT_1:def 19 :: thesis: verum

end;

suppose not i in dom p ; :: thesis: Replace (p,i,a) is D -valued

then Replace (p,i,a) = p by FUNCT_7:def 3;
hence rng (Replace (p,i,a)) c= D by RELAT_1:def 19; :: according to RELAT_1:def 19 :: thesis: verum

end;

end;