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

{} 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