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

suppose n in dom f ; :: thesis: f . n is FinSequence of D

then f . n in rng f by FUNCT_1:3;
hence f . n is FinSequence of D by FINSEQ_2:def 3; :: thesis: verum

end;

suppose not n in dom f ; :: thesis: f . n is FinSequence of D

then f . n = <*> D by FUNCT_1:def 2;
hence f . n is FinSequence of D ; :: thesis: verum

end;

end;