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

let x be object ; :: thesis: ( x in dom (g *. f) implies (g *. f) . x is Function )
reconsider xx = x as set by TARSKI:1;
assume x in dom (g *. f) ; :: thesis: (g *. f) . x is Function
then x in dom f by FOMODEL2:def 6;
then (g *. f) . x = g * (f . xx) by FOMODEL2:def 6;
hence (g *. f) . x is Function ; :: thesis: verum

end;

hence g *. f is Function-yielding by FUNCOP_1:def 6; :: thesis: verum