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 )
A1: dom (id X) = X ;
assume A2: dom f = X ; :: thesis: X -indexing f = f
thus X -indexing f = f by A2, A1, FUNCT_4:19; :: thesis: verum