set F = |[f]|;

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

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

proof

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