let X be set ; :: thesis: for x being object holds dom <:(X --> x),(id X):> = X
let x be object ; :: thesis: dom <:(X --> x),(id X):> = X
thus dom <:(X --> x),(id X):> = (dom (X --> x)) /\ (dom (id X)) by FUNCT_3:def 7
.= X ; :: thesis: verum