set h = <:f,(id X):>;

now :: thesis: for x1, x2 being object st x1 in dom <:f,(id X):> & x2 in dom <:f,(id X):> & <:f,(id X):> . x1 = <:f,(id X):> . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom <:f,(id X):> & x2 in dom <:f,(id X):> & <:f,(id X):> . x1 = <:f,(id X):> . x2 implies x1 = x2 )
assume A1: ( x1 in dom <:f,(id X):> & x2 in dom <:f,(id X):> & <:f,(id X):> . x1 = <:f,(id X):> . x2 ) ; :: thesis: x1 = x2
then ( <:f,(id X):> . x1 = [(f . x1),((id X) . x1)] & <:f,(id X):> . x2 = [(f . x2),((id X) . x2)] ) by FUNCT_3:def 7;
then A2: (id X) . x1 = (id X) . x2 by A1, XTUPLE_0:1;
( x1 in (dom f) /\ (dom (id X)) & x2 in (dom f) /\ (dom (id X)) ) by A1, FUNCT_3:def 7;
then ( (id X) . x1 = x1 & (id X) . x2 = x2 ) by FUNCT_1:18;
hence x1 = x2 by A2; :: thesis: verum

end;

hence <:f,(id X):> is one-to-one by FUNCT_1:def 4; :: thesis: verum