let X, Y, Z be set ; :: thesis: for f being Function of X,Y
for g being Function of Y,Z st Z <> {} & rng (g * f) = Z & g is one-to-one holds
rng f = Y
let f be Function of X,Y; :: thesis: for g being Function of Y,Z st Z <> {} & rng (g * f) = Z & g is one-to-one holds
rng f = Y
let g be Function of Y,Z; :: thesis: ( Z <> {} & rng (g * f) = Z & g is one-to-one implies rng f = Y )
assume that
A1: Z <> {} and
A2: rng (g * f) = Z and
A3: g is one-to-one ; :: thesis: rng f = Y
A4: dom g = Y by A1, Def1;
rng (g * f) c= rng g by RELAT_1:26;
then rng g = rng (g * f) by A2;
then Y c= rng f by A3, A4, FUNCT_1:29;
hence rng f = Y ; :: thesis: verum