theorem :: NOMIN_1:61

for a being object
for A being set
for V being non empty set
for v1, v2 being Element of V st a is TypeSCNominativeData of V,A holds
naming (V,A,<*v1,v2*>,a) = v1 .--> (v2 .--> a)