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