let F, G be Function of [:(Pr (ND (V,A))),(FPrg (ND (V,A))):],(Pr (ND (V,A))); ( ( 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)) = H1(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)) = H1(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) ) )
; F = G
let a, b be set ; BINOP_1:def 21 ( 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))
; ( 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))
; F . (a,b) = G . (a,b)
then reconsider f = b as SCBinominativeFunction of V,A by PARTFUN1:46;
A16:
dom (F . (a,b)) = H1(p,f)
by A14;
hence
dom (F . (a,b)) = dom (G . (a,b))
by A15; FUNCT_1:def 11 for b1 being object holds
( not b1 in dom (F . (a,b)) or (F . (a,b)) . b1 = (G . (a,b)) . b1 )
let z be object ; ( not z in dom (F . (a,b)) or (F . (a,b)) . z = (G . (a,b)) . z )
assume
z in dom (F . (a,b))
; (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; verum