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 by RELAT_1:71;
assume A2: dom f = X ; :: thesis: X -indexing f = f
then f | X = f by RELAT_1:97;
hence X -indexing f = f by A2, A1, FUNCT_4:20; :: thesis: verum