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:53;
hence F " {y} c= (G * F) " {(G . y)} by SETWISEO:13; :: thesis: verum