<:(id X),f:> = <:f,(id X):> ~ by FUNCOP_1:2;
hence <:(id X),f:> is one-to-one ; :: thesis: verum