let F, G be Function of (FPrg (ND (V,A))),(FPrg (ND (V,A))); :: thesis: ( ( for f being SCBinominativeFunction of V,A holds
( dom (F . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (F . f) holds
(F . f) . d = local_overlapping (V,A,d,(f . d),v) ) ) ) & ( for f being SCBinominativeFunction of V,A holds
( dom (G . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (G . f) holds
(G . f) . d = local_overlapping (V,A,d,(f . d),v) ) ) ) implies F = G )
assume that
A7: for f being SCBinominativeFunction of V,A holds
( dom (F . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (F . f) holds
(F . f) . d = local_overlapping (V,A,d,(f . d),v) ) ) and
A8: for f being SCBinominativeFunction of V,A holds
( dom (G . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (G . f) holds
(G . f) . d = local_overlapping (V,A,d,(f . d),v) ) ) ; :: thesis: F = G
let f be Element of FPrg (ND (V,A)); :: according to FUNCT_2:def 8 :: thesis: F . f = G . f
A9: f is SCBinominativeFunction of V,A by PARTFUN1:46;
hence A10: dom (F . f) = dom f by A7
.= dom (G . f) by A8, A9 ;
:: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (F . f) or (F . f) . b₁ = (G . f) . b₁ )
let d be object ; :: thesis: ( not d in dom (F . f) or (F . f) . d = (G . f) . d )
assume A11: d in dom (F . f) ; :: thesis: (F . f) . d = (G . f) . d
dom (F . f) c= ND (V,A) by RELAT_1:def 18;
then A12: d is TypeSCNominativeData of V,A by A11, NOMIN_1:39;
hence (F . f) . d = local_overlapping (V,A,d,(f . d),v) by A7, A9, A11
.= (G . f) . d by A8, A9, A10, A11, A12 ;
:: thesis: verum