theorem :: DBLSEQ_3:59

for C, D being non empty set
for F1 being without-infty Function of [:C,D:],ExtREAL
for 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)) & ProjMap1 ((F2 - F1),c) = (ProjMap1 (F2,c)) - (ProjMap1 (F1,c)) )