let F, G be Function of [:(Pr (ND (V,A))),(FPrg (ND (V,A))):],(Pr (ND (V,A))); :: thesis: ( ( for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A holds
( dom (F . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds
F . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) ) ) & ( for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A holds
( dom (G . (p,f)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,(f . d),v) in dom p & d in dom f ) } & ( for d being TypeSCNominativeData of V,A st d in dom f holds
G . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) ) ) implies F = G )
assume that
A14: for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A holds
( dom (F . (p,f)) = H₁(p,f) & ( for d being TypeSCNominativeData of V,A st d in dom f holds
F . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) ) and
A15: for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A holds
( dom (G . (p,f)) = H₁(p,f) & ( for d being TypeSCNominativeData of V,A st d in dom f holds
G . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) ) ) ; :: thesis: F = G
let a, b be set ; :: according to BINOP_1:def 21 :: thesis: ( not a in Pr (ND (V,A)) or not b in FPrg (ND (V,A)) or F . (a,b) = G . (a,b) )
assume a in Pr (ND (V,A)) ; :: thesis: ( not b in FPrg (ND (V,A)) or F . (a,b) = G . (a,b) )
then reconsider p = a as SCPartialNominativePredicate of V,A by PARTFUN1:46;
assume b in FPrg (ND (V,A)) ; :: thesis: F . (a,b) = G . (a,b)
then reconsider f = b as SCBinominativeFunction of V,A by PARTFUN1:46;
A16: dom (F . (a,b)) = H₁(p,f) by A14;
hence dom (F . (a,b)) = dom (G . (a,b)) by A15; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (F . (a,b)) or (F . (a,b)) . b₁ = (G . (a,b)) . b₁ )
let z be object ; :: thesis: ( not z in dom (F . (a,b)) or (F . (a,b)) . z = (G . (a,b)) . z )
assume z in dom (F . (a,b)) ; :: thesis: (F . (a,b)) . z = (G . (a,b)) . z
then consider d being TypeSCNominativeData of V,A such that
A17: ( z = d & local_overlapping (V,A,d,(f . d),v) in dom p ) and
A18: d in dom f by A16;
A19: G . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) by A15, A18;
F . (p,f),d =~ p, local_overlapping (V,A,d,(f . d),v) by A14, A18;
hence (F . (a,b)) . z = (G . (a,b)) . z by A17, A19; :: thesis: verum