theorem Th25: :: NOMIN_2:26

for v being object
for V, A being set
for d being TypeSCNominativeData of V,A
for f being SCBinominativeFunction of V,A holds rng (NDdataSeq (<*f*>,<*v*>,d)) = v .--> (f . d)