set F = |[f]|;
rng |[f]| c= the carrier of (TOP-REAL 1)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng |[f]| or y in the carrier of (TOP-REAL 1) )
assume y in rng |[f]| ; :: thesis: y in the carrier of (TOP-REAL 1)
then consider x being object such that
A1: x in dom |[f]| and
A2: |[f]| . x = y by FUNCT_1:def 3;
|[f]| . x = |[(f . x)]| by A1, Def1;
hence y in the carrier of (TOP-REAL 1) by A2; :: thesis: verum

end;

hence |[f]| is the carrier of (TOP-REAL 1) -valued by RELAT_1:def 19; :: thesis: verum