let X be set ; :: thesis: for Y, Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z st f is onto & g is onto holds
g * f is onto
let Y, Z be non empty set ; :: thesis: for f being Function of X,Y
for g being Function of Y,Z st f is onto & g is onto holds
g * f is onto
let f be Function of X,Y; :: thesis: for g being Function of Y,Z st f is onto & g is onto holds
g * f is onto
let g be Function of Y,Z; :: thesis: ( f is onto & g is onto implies g * f is onto )
assume that
A1: f is onto and
A2: g is onto ; :: thesis: g * f is onto
rng f = Y by A1
.= dom g by Def1 ;
then rng (g * f) = rng g by RELAT_1:28
.= Z by A2 ;
hence g * f is onto ; :: thesis: verum