theorem :: DBLSEQ_3:58

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