( dom (g *. f) = dom f & dom f = Seg (len f) ) by FOMODEL2:def 6, FINSEQ_1:def 3;
hence g *. f is FinSequence-like ; :: thesis: verum