let A be set ; :: thesis: for f being Function
for g being A -defined Function holds f,f +* g equal_outside A
let f be Function; :: thesis: for g being A -defined Function holds f,f +* g equal_outside A
let g be A -defined Function; :: thesis: f,f +* g equal_outside A
dom g c= A by RELAT_1:def 18;
hence f,f +* g equal_outside A by Th31; :: thesis: verum