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;