theorem :: DBLSEQ_3:60

for C, D being non empty set
for F1 being V183() Function of [:C,D:],ExtREAL
for F2 being V184() 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)) )