let V, A be set ; :: thesis: for n being Nat st 1 <= n holds
{} in (FNDSC (V,A)) . n
let n be Nat; :: thesis: ( 1 <= n implies {} in (FNDSC (V,A)) . n )
set F = FNDSC (V,A);
assume 1 <= n ; :: thesis: {} in (FNDSC (V,A)) . n
then reconsider m = n - 1 as Element of NAT by INT_1:5;
(FNDSC (V,A)) . (m + 1) = NDSS (V,(A \/ ((FNDSC (V,A)) . m))) by Def3;
hence {} in (FNDSC (V,A)) . n by Th6; :: thesis: verum