for D being non empty set
for f being BinominativeFunction of D holds id (field f) is BinominativeFunction of D