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 by RELAT_1:71;
then Y c= rng f by RELAT_1:45;
hence rng f = Y by XBOOLE_0:def 10; :: thesis: verum