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 3;
then {d} c= D by ZFMISC_1:31;
then A2: ( (rng f) \/ (rng (i .--> d)) = (rng f) \/ {d} & (rng f) \/ {d} c= D ) by FUNCOP_1:8, XBOOLE_1:8;
f +* (i,d) = f +* (i .--> d) by A1, Def2;
then rng (f +* (i,d)) c= (rng f) \/ (rng (i .--> d)) by FUNCT_4:17;
then rng (f +* (i,d)) c= D by A2;
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 Def2; :: thesis: verum

end;

end;