let V, A be set ; :: thesis: (FNDSC (V,A)) . 1 = NDSS (V,A)
( (FNDSC (V,A)) . (0 + 1) = NDSS (V,(A \/ ((FNDSC (V,A)) . 0))) & (FNDSC (V,A)) . 0 = A ) by Def3;
hence (FNDSC (V,A)) . 1 = NDSS (V,A) ; :: thesis: verum