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 Th130;
then A1: h +* f,h equal_outside A by Th26;
h,h +* g equal_outside A by Th130;
hence h +* f,h +* g equal_outside A by A1, Th27; :: thesis: verum