let f be Function; :: thesis: for A being set holds f +* (f | A) = f
let A be set ; :: thesis: f +* (f | A) = f
f | A c= f by RELAT_1:59;
hence f +* (f | A) = f by Lm79; :: thesis: verum