defpred S₁[ object , object ] means ex d1 being NonatomicND of V,A ex d2 being object st
( $1 = [d1,d2] & $2 = local_overlapping (V,A,d1,d2,v) );
A1: for x being object st x in [:((ND (V,A)) \ A),(ND (V,A)):] holds
ex y being object st
( y in ND (V,A) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in [:((ND (V,A)) \ A),(ND (V,A)):] implies ex y being object st
( y in ND (V,A) & S₁[x,y] ) )
assume x in [:((ND (V,A)) \ A),(ND (V,A)):] ; :: thesis: ex y being object st
( y in ND (V,A) & S₁[x,y] )
then consider d1, d2 being object such that
A2: ( d1 in (ND (V,A)) \ A & d2 in ND (V,A) ) and
A3: x = [d1,d2] by ZFMISC_1:def 2;
reconsider d1 = d1 as NonatomicND of V,A by A2, Th43;
take local_overlapping (V,A,d1,d2,v) ; :: thesis: ( local_overlapping (V,A,d1,d2,v) in ND (V,A) & S₁[x, local_overlapping (V,A,d1,d2,v)] )
thus ( local_overlapping (V,A,d1,d2,v) in ND (V,A) & S₁[x, local_overlapping (V,A,d1,d2,v)] ) by A3; :: thesis: verum

end;

consider f being Function such that
A4: dom f = [:((ND (V,A)) \ A),(ND (V,A)):] and
A5: rng f c= ND (V,A) and
A6: for x being object st x in [:((ND (V,A)) \ A),(ND (V,A)):] holds
S₁[x,f . x] from FUNCT_1:sch 6(A1);
reconsider f = f as PartFunc of [:(ND (V,A)),(ND (V,A)):],(ND (V,A)) by A4, A5, RELSET_1:4, ZFMISC_1:96;
take f ; :: thesis: ( dom f = [:((ND (V,A)) \ A),(ND (V,A)):] & ( for d1 being NonatomicND of V,A
for d2 being object st not d1 in A & d2 in ND (V,A) holds
f . [d1,d2] = local_overlapping (V,A,d1,d2,v) ) )
thus dom f = [:((ND (V,A)) \ A),(ND (V,A)):] by A4; :: thesis: for d1 being NonatomicND of V,A
for d2 being object st not d1 in A & d2 in ND (V,A) holds
f . [d1,d2] = local_overlapping (V,A,d1,d2,v)
let D1 be NonatomicND of V,A; :: thesis: for d2 being object st not D1 in A & d2 in ND (V,A) holds
f . [D1,d2] = local_overlapping (V,A,D1,d2,v)
let D2 be object ; :: thesis: ( not D1 in A & D2 in ND (V,A) implies f . [D1,D2] = local_overlapping (V,A,D1,D2,v) )
set D = [D1,D2];
assume ( not D1 in A & D2 in ND (V,A) ) ; :: thesis: f . [D1,D2] = local_overlapping (V,A,D1,D2,v)
then ( D1 in (ND (V,A)) \ A & D2 in ND (V,A) ) by Th42;
then [D1,D2] in dom f by A4, ZFMISC_1:def 2;
then consider d1 being NonatomicND of V,A, d2 being object such that
A7: [D1,D2] = [d1,d2] and
A8: f . [D1,D2] = local_overlapping (V,A,d1,d2,v) by A4, A6;
( d1 = D1 & d2 = D2 ) by A7, XTUPLE_0:1;
hence f . [D1,D2] = local_overlapping (V,A,D1,D2,v) by A8; :: thesis: verum