set RR = id (X /\ (dom R));
set I = id X;
A1: R = (id X) | (dom R) by GRFUNC_1:23
.= id (X /\ (dom R)) by Lm67 ;
thus R ~ = R by A1; :: thesis: verum