let A be set ; :: thesis: for f, g being A -defined Function
for h being Function holds h +* f,h +* g equal_outside A
let f, g be A -defined Function; :: thesis: for h being Function holds h +* f,h +* g equal_outside A
let h be Function; :: thesis: h +* f,h +* g equal_outside A
h,h +* f equal_outside A by Th132;
then A1: h +* f,h equal_outside A by Th28;
h,h +* g equal_outside A by Th132;
hence h +* f,h +* g equal_outside A by A1, Th29; :: thesis: verum