defpred S₁[ object , object ] means ex D being NonatomicND of V,A st
( D = $1 & $2 = denaming (v,D) );
A1: for x being object st x in { d where d is NonatomicND of V,A : v in dom d } holds
ex y being object st
( y in ND (V,A) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in { d where d is NonatomicND of V,A : v in dom d } implies ex y being object st
( y in ND (V,A) & S₁[x,y] ) )
assume x in { d where d is NonatomicND of V,A : v in dom d } ; :: thesis: ex y being object st
( y in ND (V,A) & S₁[x,y] )
then consider d being NonatomicND of V,A such that
A2: x = d and
v in dom d ;
take denaming (v,d) ; :: thesis: ( denaming (v,d) in ND (V,A) & S₁[x, denaming (v,d)] )
thus ( denaming (v,d) in ND (V,A) & S₁[x, denaming (v,d)] ) by A2; :: thesis: verum

end;

consider f being Function such that
A3: dom f = { d where d is NonatomicND of V,A : v in dom d } and
A4: rng f c= ND (V,A) and
A5: for x being object st x in { d where d is NonatomicND of V,A : v in dom d } holds
S₁[x,f . x] from FUNCT_1:sch 6(A1);
{ d where d is NonatomicND of V,A : v in dom d } c= ND (V,A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d where d is NonatomicND of V,A : v in dom d } or x in ND (V,A) )
assume x in { d where d is NonatomicND of V,A : v in dom d } ; :: thesis: x in ND (V,A)
then ex d being NonatomicND of V,A st
( x = d & v in dom d ) ;
hence x in ND (V,A) ; :: thesis: verum

end;

then reconsider f = f as PartFunc of (ND (V,A)),(ND (V,A)) by A3, A4, RELSET_1:4;
take f ; :: thesis: ( dom f = { d where d is NonatomicND of V,A : v in dom d } & ( for D being NonatomicND of V,A st D in dom f holds
f . D = denaming (v,D) ) )
thus dom f = { d where d is NonatomicND of V,A : v in dom d } by A3; :: thesis: for D being NonatomicND of V,A st D in dom f holds
f . D = denaming (v,D)
let D be NonatomicND of V,A; :: thesis: ( D in dom f implies f . D = denaming (v,D) )
assume D in dom f ; :: thesis: f . D = denaming (v,D)
then S₁[D,f . D] by A3, A5;
hence f . D = denaming (v,D) ; :: thesis: verum