let V, A be set ; :: thesis: for D being finite Function st dom D c= V & rng D c= ND (V,A) holds
D is NonatomicND of V,A
let D be finite Function; :: thesis: ( dom D c= V & rng D c= ND (V,A) implies D is NonatomicND of V,A )
assume that
A1: dom D c= V and
A2: rng D c= ND (V,A) ; :: thesis: D is NonatomicND of V,A
defpred S₁[ set ] means $1 is NonatomicND of V,A;
A3: D is finite ;
A4: S₁[ {} ] by NOMIN_1:30;
A5: for x, B being set st x in D & B c= D & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in D & B c= D & S₁[B] implies S₁[B \/ {x}] )
assume that
A6: x in D and
A7: B c= D ; :: thesis: ( not S₁[B] or S₁[B \/ {x}] )
assume S₁[B] ; :: thesis: S₁[B \/ {x}]
then reconsider B = B as NonatomicND of V,A ;
consider a, b being object such that
A8: x = [a,b] by A6, RELAT_1:def 1;
A9: a in dom D by A6, A8, XTUPLE_0:def 12;
b in rng D by A6, A8, XTUPLE_0:def 13;
then b is TypeSCNominativeData of V,A by A2, NOMIN_1:39;
then A10: {[a,b]} is NonatomicND of V,A by A1, A9, Th5;
{x} c= D by A6, ZFMISC_1:31;
then B \/ {[a,b]} is Function by A7, A8, GRFUNC_1:14;
hence S₁[B \/ {x}] by A8, A10, NOMIN_1:36, PARTFUN1:51; :: thesis: verum

end;

S₁[D] from FINSET_1:sch 2(A3, A4, A5);
hence D is NonatomicND of V,A ; :: thesis: verum