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:59;
hence (f | A) +* f = f by Th103; :: thesis: verum