now

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

suppose i in dom p ; :: thesis: rng (Replace p,i,a) c= D

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 ( rng (i .--> a) c= D & rng p c= D ) by ORDINAL1:def 8, ZFMISC_1:37;
then (rng p) \/ (rng (i .--> a)) c= D by XBOOLE_1:8;
hence rng (Replace p,i,a) c= D by A1, XBOOLE_1:1; :: thesis: verum

end;

suppose not i in dom p ; :: thesis: rng (Replace p,i,a) c= D

then Replace p,i,a = p by FUNCT_7:def 3;
hence rng (Replace p,i,a) c= D by ORDINAL1:def 8; :: thesis: verum

end;

end;

end;

hence Replace p,i,a is XFinSequence of D by ORDINAL1:def 8; :: thesis: verum