reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
A1: ( g1 is continuous & g2 is continuous ) by Th23;
g1 + g2 = f1 + f2 by Th5;
hence for b₁ being PartFunc of REAL,(REAL n) st b₁ = f1 + f2 holds
b₁ is continuous by A1, Th23; :: thesis: verum