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