let F, G be Function of [:(FPrg (ND (V,A))),(product g):],(FPrg (ND (V,A))); ( ( 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)) = H1(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)) = H1(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))) ) )
; F = G
let a, b be set ; BINOP_1:def 21 ( 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))
; ( 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
; F . (a,b) = G . (a,b)
then A18:
dom (F . (a,b)) = H1(f)
by A15;
hence
dom (F . (a,b)) = dom (G . (a,b))
by A16, A17; 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
A19:
( z = d & global_overlapping (V,A,d,(NDentry (g,X,d))) in dom f & S1[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; verum