theorem :: NCFCONT1:102

for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X, X1 being set
for f1, f2 being PartFunc of RNS,CNS st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds
f1 + f2 is_Lipschitzian_on X /\ X1