let f be Function; :: thesis: rng (.: f) c= bool (rng f)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (.: f) or y in bool (rng f) )
reconsider yy = y as set by TARSKI:1;
assume y in rng (.: f) ; :: thesis: y in bool (rng f)
then consider x being object such that
A1: ( x in dom (.: f) & y = (.: f) . x ) by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
y = f .: x by A1, Th7;
then yy c= rng f by RELAT_1:111;
hence y in bool (rng f) ; :: thesis: verum