dom F = C1 by FUNCT_2:def 1;
then consider y being Element of C1 such that
A1: y in dom F by SUBSET_1:4;
F . y in rng F by A1, FUNCT_1:def 3;
hence not rng F is empty ; :: thesis: verum