let x be object ; :: thesis: for f being Function-yielding Function
for g being Function holds (g *. f) . x = g * (f . x)
let f be Function-yielding Function; :: thesis: for g being Function holds (g *. f) . x = g * (f . x)
let g be Function; :: thesis: (g *. f) . x = g * (f . x)

per cases ( x in dom f or not x in dom f ) ;

suppose x in dom f ; :: thesis: (g *. f) . x = g * (f . x)

hence (g *. f) . x = g * (f . x) by FOMODEL2:def 6; :: thesis: verum

end;

suppose not x in dom f ; :: thesis: (g *. f) . x = g * (f . x)

then ( not x in dom (g *. f) & f . x = {} ) by FOMODEL2:def 6, FUNCT_1:def 2;
then ( (g *. f) . x = {} & g * (f . x) = {} ) by FUNCT_1:def 2;
hence (g *. f) . x = g * (f . x) ; :: thesis: verum

end;

end;