theorem :: DBLSEQ_2:20

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