let f, g be Function of (Pr (ND (V,A))),(Pr (ND (V,A))); :: thesis: ( ( 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) = H₁(p) & ( for d being TypeSCNominativeData of V,A holds
( ( S₁[d,p] implies (f . p) . d = TRUE ) & ( S₂[d,p] implies (f . p) . d = FALSE ) ) ) ) and
A16: for p being SCPartialNominativePredicate of V,A holds
( dom (g . p) = H₁(p) & ( for d being TypeSCNominativeData of V,A holds
( ( S₁[d,p] implies (g . p) . d = TRUE ) & ( S₂[d,p] implies (g . p) . d = FALSE ) ) ) ) ; :: thesis: f = g
let x be Element of Pr (ND (V,A)); :: according to FUNCT_2:def 8 :: thesis: f . x = g . x
reconsider p = x as SCPartialNominativePredicate of V,A by PARTFUN1:46;
A17: dom (f . x) = H₁(p) by A15;
hence dom (f . x) = dom (g . x) by A16; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (f . x) or (f . x) . b₁ = (g . x) . b₁ )
let a be object ; :: thesis: ( not a in dom (f . x) or (f . x) . a = (g . x) . a )
assume a in dom (f . x) ; :: thesis: (f . x) . a = (g . x) . a
then consider d being TypeSCNominativeData of V,A such that
A18: a = d and
A19: ( S₁[d,p] or S₂[d,p] ) by A17;

per cases ( S₁[d,p] or S₂[d,p] ) by A19;

suppose A20: S₁[d,p] ; :: thesis: (f . x) . a = (g . x) . a

thus (f . x) . a = TRUE by A15, A18, A20
.= (g . x) . a by A16, A18, A20 ; :: thesis: verum

end;

suppose A21: S₂[d,p] ; :: thesis: (f . x) . a = (g . x) . a

thus (f . x) . a = FALSE by A15, A18, A21
.= (g . x) . a by A16, A18, A21 ; :: thesis: verum

end;

end;