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