let x be set ; :: according to CAT_5:def 4 :: thesis: ( not x in rng f or x is CatStr )
assume x in rng f ; :: thesis: x is CatStr
then ex y being object st
( y in dom f & x = f . y ) by FUNCT_1:def 3;
hence x is CatStr by Def1; :: thesis: verum