let V, A be set ; :: thesis: A c= Union (FNDSC (V,A))
set F = FNDSC (V,A);
A1: A = (FNDSC (V,A)) . 0 by Def3;
dom (FNDSC (V,A)) = NAT by Def3;
then (FNDSC (V,A)) . 0 in rng (FNDSC (V,A)) by FUNCT_1:def 3;
hence A c= Union (FNDSC (V,A)) by A1, ZFMISC_1:74; :: thesis: verum