set gf = g *. f;
reconsider X = x as set by TARSKI:1;
A5: dom (g *. f) = dom f by FOMODEL2:def 6;

per cases ( x in dom (g *. f) or not x in dom (g *. f) ) ;

suppose A6: x in dom (g *. f) ; :: thesis: (g *. f) . x is len (f . x) -element

then A7: (g *. f) . x = g * (f . X) by A5, FOMODEL2:def 6;
f . x in rng f by A6, A5, FUNCT_1:def 3;
then reconsider fx = f . X as FinSequence of dom g by FINSEQ_1:def 11;
rng fx c= dom g ;
then dom ((g *. f) . x) = dom fx by RELAT_1:27, A7;
then len ((g *. f) . X) = len fx by FINSEQ_3:29;
hence (g *. f) . x is len (f . x) -element by CARD_1:def 7; :: thesis: verum

end;

suppose not x in dom (g *. f) ; :: thesis: (g *. f) . x is len (f . x) -element

then ( (g *. f) . x = {} & f . x = {} ) by A5, FUNCT_1:def 2;
hence (g *. f) . x is len (f . x) -element ; :: thesis: verum

end;

end;