theorem :: DBLSEQ_3:60

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 d being Element of D holds
( ProjMap2 ((F1 - F2),d) = (ProjMap2 (F1,d)) - (ProjMap2 (F2,d)) & ProjMap2 ((F2 - F1),d) = (ProjMap2 (F2,d)) - (ProjMap2 (F1,d)) )