let f be Function; :: thesis: rng (" f) c= bool (dom f)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (" f) or x in bool (dom f) )
assume x in rng (" f) ; :: thesis: x in bool (dom f)
then consider y being set such that
A1: y in dom (" f) and
A2: x = (" f) . y by FUNCT_1:def 5;
x = f " y by A1, A2, Th24;
then x c= dom f by RELAT_1:167;
hence x in bool (dom f) ; :: thesis: verum