set gf = g *. f;

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

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

end;

hence g *. f is complex-functions-valued by VALUED_2:def 26; :: thesis: verum