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

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