set gf = g *. f;

now :: thesis: for x being object st x in dom (g *. f) holds
(g *. f) . x is FinSequence

let x be object ; :: thesis: ( x in dom (g *. f) implies (g *. f) . x is FinSequence )
reconsider X = x as set by TARSKI:1;
A1: dom (g *. f) = dom f by FOMODEL2:def 6;
assume A2: x in dom (g *. f) ; :: thesis: (g *. f) . x is FinSequence
then A3: (g *. f) . x = g * (f . X) by A1, FOMODEL2:def 6;
f . x in rng f by A2, A1, FUNCT_1:def 3;
then reconsider fx = f . X as FinSequence of dom g by FINSEQ_1:def 11;
A4: rng fx c= dom g ;
dom fx = Seg (len fx) by FINSEQ_1:def 3;
hence (g *. f) . x is FinSequence by FINSEQ_1:def 2, A3, A4, RELAT_1:27; :: thesis: verum

end;

hence g *. f is FinSequence-yielding by PRE_POLY:def 3; :: thesis: verum