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