let f be Function-yielding Function; :: thesis: for g being Function holds Values (g *. f) = g .: (Values f)
let g be Function; :: thesis: Values (g *. f) = g .: (Values f)
set gf = g *. f;
A1: dom (g *. f) = dom f by FOMODEL2:def 6;
thus Values (g *. f) c= g .: (Values f) :: according to XBOOLE_0:def 10 :: thesis: g .: (Values f) c= Values (g *. f)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Values (g *. f) or a in g .: (Values f) )
assume a in Values (g *. f) ; :: thesis: a in g .: (Values f)
then consider x, y being object such that
A2: ( x in dom (g *. f) & y in dom ((g *. f) . x) & a = ((g *. f) . x) . y ) by Th1;
(g *. f) . x = g * (f . x) by A1, FOMODEL2:def 6, A2;
then A3: ( ((g *. f) . x) . y = g . ((f . x) . y) & y in dom (f . x) & (f . x) . y in dom g ) by A2, FUNCT_1:11, FUNCT_1:12;
then (f . x) . y in Values f by A1, A2, Th1;
hence a in g .: (Values f) by A3, A2, FUNCT_1:def 6; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in g .: (Values f) or a in Values (g *. f) )
assume a in g .: (Values f) ; :: thesis: a in Values (g *. f)
then consider b being object such that
A4: ( b in dom g & b in Values f & g . b = a ) by FUNCT_1:def 6;
consider x, y being object such that
A5: ( x in dom f & y in dom (f . x) & b = (f . x) . y ) by A4, Th1;
A6: ( g . ((f . x) . y) = (g * (f . x)) . y & y in dom (g * (f . x)) ) by A4, A5, FUNCT_1:11, FUNCT_1:13;
( g * (f . x) = (g *. f) . x & x in dom (g *. f) ) by A5, FOMODEL2:def 6;
hence a in Values (g *. f) by Th1, A4, A5, A6; :: thesis: verum