defpred S_{1}[ 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_{1}[x,y] )

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_{1}[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)

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_{1}[D,f . D]
by A3, A5;

hence f . D = denaming (v,D) ; :: thesis: verum

( 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

proof

consider f being Function such that
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_{1}[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_{1}[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_{1}[x, denaming (v,d)] )

thus ( denaming (v,d) in ND (V,A) & S_{1}[x, denaming (v,d)] )
by A2; :: thesis: verum

end;( y in ND (V,A) & S

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

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

thus ( denaming (v,d) in ND (V,A) & S

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

{ d where d is NonatomicND of V,A : v in dom d } c= ND (V,A)

proof

then reconsider f = f as PartFunc of (ND (V,A)),(ND (V,A)) by A3, A4, RELSET_1:4;
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;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

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

hence f . D = denaming (v,D) ; :: thesis: verum