let X be set ; :: thesis: for f being Function holds X -indexing ((id X) +* f) = X -indexing f
let f be Function; :: thesis: X -indexing ((id X) +* f) = X -indexing f
A1: dom (id X) = X by RELAT_1:71;
thus X -indexing ((id X) +* f) = (id X) +* (((id X) | X) +* (f | X)) by FUNCT_4:75
.= (id X) +* ((id X) +* (f | X)) by A1, RELAT_1:97
.= ((id X) +* (id X)) +* (f | X) by FUNCT_4:15
.= X -indexing f ; :: thesis: verum