let F, G be Function of [:(Pr (ND (V,A))),(product g):],(Pr (ND (V,A))); :: thesis: ( ( for p being SCPartialNominativePredicate of V,A
for x being Element of product g holds
( dom (F . (p,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds
F . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) ) & ( for p being SCPartialNominativePredicate of V,A
for x being Element of product g holds
( dom (G . (p,x)) = { d where d is TypeSCNominativeData of V,A : ( global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p & d in_doms g ) } & ( for d being TypeSCNominativeData of V,A st d in_doms g holds
G . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) ) implies F = G )
assume that
A16: for p being SCPartialNominativePredicate of V,A
for x being Element of product g holds
( dom (F . (p,x)) = H₁(p) & ( for d being TypeSCNominativeData of V,A st S₁[d] holds
F . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) and
A17: for p being SCPartialNominativePredicate of V,A
for x being Element of product g holds
( dom (G . (p,x)) = H₁(p) & ( for d being TypeSCNominativeData of V,A st S₁[d] holds
G . (p,x),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) ) ) ; :: 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 product g or F . (a,b) = G . (a,b) )
assume a in Pr (ND (V,A)) ; :: thesis: ( not b in product g or F . (a,b) = G . (a,b) )
then reconsider p = a as SCPartialNominativePredicate of V,A by PARTFUN1:46;
assume A18: b in product g ; :: thesis: F . (a,b) = G . (a,b)
then A19: dom (F . (a,b)) = H₁(p) by A16;
hence dom (F . (a,b)) = dom (G . (a,b)) by A17, A18; :: 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 A20: 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
A21: d = z and
global_overlapping (V,A,d,(NDentry (g,X,d))) in dom p and
A22: S₁[d] by A19;
A23: G . (p,b),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) by A17, A18, A22;
F . (p,b),d =~ p, global_overlapping (V,A,d,(NDentry (g,X,d))) by A16, A18, A22;
hence (F . (a,b)) . z = (G . (a,b)) . z by A20, A23, A21; :: thesis: verum