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

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