let D be non empty set ; :: thesis: for f being BinominativeFunction of D holds id (field f) is BinominativeFunction of D
let f be BinominativeFunction of D; :: thesis: id (field f) is BinominativeFunction of D
( dom f c= D & rng f c= D ) by RELAT_1:def 19;
then reconsider X = field f as Subset of D by XBOOLE_1:8;
id X is BinominativeFunction of D ;
hence id (field f) is BinominativeFunction of D ; :: thesis: verum