( dom (g *. f) = dom f & dom f = Seg (len f) ) by FOMODEL2:def 6, FINSEQ_1:def 3;
then len (g *. f) = len f by FINSEQ_3:29;
hence g *. f is len f -element by CARD_1:def 7; :: thesis: verum