set x = the Element of dom r;
r . the Element of dom r in rng r by FUNCT_1:3;
hence not rng r is empty ; :: thesis: verum