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

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

( $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

proof

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

assume x in [:((ND (V,A)) \ A),(ND (V,A)):] ; :: thesis: ex y being object st

( y in ND (V,A) & S_{1}[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_{1}[x, local_overlapping (V,A,d1,d2,v)] )

thus ( local_overlapping (V,A,d1,d2,v) in ND (V,A) & S_{1}[x, local_overlapping (V,A,d1,d2,v)] )
by A3; :: thesis: verum

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

assume x in [:((ND (V,A)) \ A),(ND (V,A)):] ; :: thesis: ex y being object st

( y in ND (V,A) & S

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

thus ( local_overlapping (V,A,d1,d2,v) in ND (V,A) & S

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

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