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:45;
thus X -indexing ((id X) +* f) = (id X) +* (((id X) | X) +* (f | X)) by FUNCT_4:71
.= (id X) +* ((id X) +* (f | X)) by A1, RELAT_1:68
.= ((id X) +* (id X)) +* (f | X) by FUNCT_4:14
.= X -indexing f ; :: thesis: verum