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:18;
rng (i .--> a) = {a} by FUNCOP_1:14;
then A2: rng (i .--> a) c= D by ZFMISC_1:37;
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, XBOOLE_1:1; :: 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;