let f, g be Function of (ND (V,A)),(ND (V,A)); :: thesis: ( ( for D being TypeSCNominativeData of V,A holds f . D = naming (V,A,v,D) ) & ( for D being TypeSCNominativeData of V,A holds g . D = naming (V,A,v,D) ) implies f = g )
assume that
A3: for D being TypeSCNominativeData of V,A holds f . D = naming (V,A,v,D) and
A4: for D being TypeSCNominativeData of V,A holds g . D = naming (V,A,v,D) ; :: thesis: f = g
let D be Element of ND (V,A); :: according to FUNCT_2:def 8 :: thesis: f . D = g . D
A5: D is TypeSCNominativeData of V,A by Th39;
hence f . D = naming (V,A,v,D) by A3
.= g . D by A4, A5 ;
:: thesis: verum