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) & x = (" f) . y ) by FUNCT_1:def 3;
x = f " y by A1, Th24;
then x c= dom f by RELAT_1:132;
hence x in bool (dom f) ; :: thesis: verum