( root-tree s in FreeGenSetNSG (f,D) & dom F = FreeGenSetNSG (f,D) ) by A1, FUNCT_2:def 1;
then ( rng F c= C & F . (root-tree s) in rng F ) by FUNCT_1:def 3, RELAT_1:def 19;
hence F . (root-tree s) is Element of C ; :: thesis: verum