theorem :: DBLSEQ_2:21

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