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