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