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

suppose A1: i in dom f ; :: thesis: f +* i,d is FinSequence of D

then f . i in rng f by FUNCT_1:def 5;
then {d} c= D by ZFMISC_1:37;
then A2: ( (rng f) \/ (rng (i .--> d)) = (rng f) \/ {d} & (rng f) \/ {d} c= D ) by FUNCOP_1:14, XBOOLE_1:8;
f +* i,d = f +* (i .--> d) by A1, Def3;
then rng (f +* i,d) c= (rng f) \/ (rng (i .--> d)) by FUNCT_4:18;
then rng (f +* i,d) c= D by A2, XBOOLE_1:1;
hence f +* i,d is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum

end;

suppose not i in dom f ; :: thesis: f +* i,d is FinSequence of D

hence f +* i,d is FinSequence of D by Def3; :: thesis: verum

end;

end;