let X, Y, Z be non empty set ; :: thesis: for y being Element of Y
for F being Function of X,Y
for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}
let y be Element of Y; :: thesis: for F being Function of X,Y
for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}
let F be Function of X,Y; :: thesis: for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}
let G be Function of Y,Z; :: thesis: F " {y} c= (G * F) " {(G . y)}
F " {y} c= (G * F) " (Im (G,y)) by FUNCT_2:44;
hence F " {y} c= (G * F) " {(G . y)} by SETWISEO:8; :: thesis: verum