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 )
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 ;
:: thesis: verum