let X be set ; :: thesis: for f being Function st dom f = X holds
X -indexing f = f
let f be Function; :: thesis: ( dom f = X implies X -indexing f = f )
assume A1: dom f = X ; :: thesis: X -indexing f = f
then ( f | X = f & dom (id X) = X & X -indexing f = (id X) +* (f | X) ) by RELAT_1:71, RELAT_1:97;
hence X -indexing f = f by A1, FUNCT_4:20; :: thesis: verum