theorem :: DBLSEQ_3:57

for C, D being non empty set
for F1, F2 being without+infty Function of [:C,D:],ExtREAL
for c being Element of C holds ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c))