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

suppose A1: n in dom g ; :: thesis: g . n is FinSequence of d

A2: rng g c= d * by FINSEQ_1:def 4;
g . n in rng g by A1, FUNCT_1:3;
then g . n is Element of d * by A2;
hence g . n is FinSequence of d ; :: thesis: verum

end;

suppose not n in dom g ; :: thesis: g . n is FinSequence of d

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

end;

end;