set g = cosec f;
thus rng (cosec 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 (cosec f) or y in REAL )
assume y in rng (cosec f) ; :: thesis: y in REAL
then consider x being object such that
A3: x in dom (cosec f) and
A4: y = (cosec f) . x by FUNCT_1:def 3;
dom (cosec f) = dom f by Def4;
then (cosec f) . x = cosec (f . x) by A3, Def4;
hence y in REAL by A4, XREAL_0:def 1; :: thesis: verum
end;