set g = cot f;
thus rng (cot f) c= REAL :: according to RELAT_1:def 19 :: thesis: verum
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (cot f) or y in REAL )
assume y in rng (cot f) ; :: thesis: y in REAL
then consider x being object such that
A1: x in dom (cot f) and
A2: y = (cot f) . x by FUNCT_1:def 3;
dom (cot f) = dom f by Def3;
then (cot f) . x = cot (f . x) by A1, Def3;
hence y in REAL by A2, XREAL_0:def 1; :: thesis: verum
end;