let X be set ; :: thesis: for f being Function st f c= id X holds
X -indexing f = id X
let f be Function; :: thesis: ( f c= id X implies X -indexing f = id X )
A1: dom (id X) = X by RELAT_1:45;
assume f c= id X ; :: thesis: X -indexing f = id X
then (id X) +* f = id X by FUNCT_4:98;
hence X -indexing f = X -indexing (id X) by Th12
.= id X by A1, Th10 ;
:: thesis: verum