set f = id X;
let a be set ; :: according to PARTIT_2:def 2 :: thesis: ( a in dom (id X) implies (id X) . ((id X) . a) = a )
assume a in dom (id X) ; :: thesis: (id X) . ((id X) . a) = a
then a in X ;
then (id X) . a = a by FUNCT_1:17;
hence (id X) . ((id X) . a) = a ; :: thesis: verum