let f, g be Function of (Pr (ND (V,A))),(Pr (ND (V,A))); ( ( for p being SCPartialNominativePredicate of V,A holds
( dom (f . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds
( ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (f . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (f . p) . d = FALSE ) ) ) ) ) & ( for p being SCPartialNominativePredicate of V,A holds
( dom (g . p) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } & ( for d being TypeSCNominativeData of V,A holds
( ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) implies (g . p) . d = TRUE ) & ( ( for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) implies (g . p) . d = FALSE ) ) ) ) ) implies f = g )
assume that
A15:
for p being SCPartialNominativePredicate of V,A holds
( dom (f . p) = H1(p) & ( for d being TypeSCNominativeData of V,A holds
( ( S1[d,p] implies (f . p) . d = TRUE ) & ( S2[d,p] implies (f . p) . d = FALSE ) ) ) )
and
A16:
for p being SCPartialNominativePredicate of V,A holds
( dom (g . p) = H1(p) & ( for d being TypeSCNominativeData of V,A holds
( ( S1[d,p] implies (g . p) . d = TRUE ) & ( S2[d,p] implies (g . p) . d = FALSE ) ) ) )
; f = g
let x be Element of Pr (ND (V,A)); FUNCT_2:def 8 f . x = g . x
reconsider p = x as SCPartialNominativePredicate of V,A by PARTFUN1:46;
A17:
dom (f . x) = H1(p)
by A15;
hence
dom (f . x) = dom (g . x)
by A16; FUNCT_1:def 11 for b1 being object holds
( not b1 in dom (f . x) or (f . x) . b1 = (g . x) . b1 )
let a be object ; ( not a in dom (f . x) or (f . x) . a = (g . x) . a )
assume
a in dom (f . x)
; (f . x) . a = (g . x) . a
then consider d being TypeSCNominativeData of V,A such that
A18:
a = d
and
A19:
( S1[d,p] or S2[d,p] )
by A17;