let X be 1-sorted ; :: thesis: for Y, Z being non empty 1-sorted
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 1-sorted ; :: 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 = the carrier of Y by A1, FUNCT_2:def 3
.= dom g by FUNCT_2:def 1 ;
then rng (g * f) = rng g by RELAT_1:47
.= the carrier of Z by A2, FUNCT_2:def 3 ;
hence g * f is onto by FUNCT_2:def 3; :: thesis: verum