let X, Y be set ; :: thesis: for f being Function of X,Y
for g being Function of Y,X st f * g = id Y holds
rng f = Y
let f be Function of X,Y; :: thesis: for g being Function of Y,X st f * g = id Y holds
rng f = Y
let g be Function of Y,X; :: thesis: ( f * g = id Y implies rng f = Y )
assume f * g = id Y ; :: thesis: rng f = Y
then rng (f * g) = Y ;
then Y c= rng f by RELAT_1:26;
hence rng f = Y ; :: thesis: verum