let C, D be non empty set ; :: thesis: 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)) )
let F1 be without-infty Function of [:C,D:],ExtREAL; :: thesis: 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)) )
let F2 be without+infty Function of [:C,D:],ExtREAL; :: thesis: 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)) )
let d be Element of D; :: thesis: ( ProjMap2 ((F1 - F2),d) = (ProjMap2 (F1,d)) - (ProjMap2 (F2,d)) & ProjMap2 ((F2 - F1),d) = (ProjMap2 (F2,d)) - (ProjMap2 (F1,d)) )
A2: ( dom (ProjMap2 ((F1 - F2),d)) = C & dom (ProjMap2 ((F2 - F1),d)) = C & dom (ProjMap2 (F1,d)) = C & dom (ProjMap2 (F2,d)) = C ) by FUNCT_2:def 1;
( {-infty} misses rng (ProjMap2 (F1,d)) & {+infty} misses rng (ProjMap2 (F2,d)) ) by ZFMISC_1:50, MESFUNC5:def 3, MESFUNC5:def 4;
then B1: ( (ProjMap2 (F1,d)) " {-infty} = {} & (ProjMap2 (F2,d)) " {+infty} = {} ) by RELAT_1:138;
then dom (ProjMap2 ((F1 - F2),d)) = ((dom (ProjMap2 (F1,d))) /\ (dom (ProjMap2 (F2,d)))) \ ((((ProjMap2 (F1,d)) " {-infty}) /\ ((ProjMap2 (F2,d)) " {-infty})) \/ (((ProjMap2 (F1,d)) " {+infty}) /\ ((ProjMap2 (F2,d)) " {+infty}))) by A2;
then A5: dom (ProjMap2 ((F1 - F2),d)) = dom ((ProjMap2 (F1,d)) - (ProjMap2 (F2,d))) by MESFUNC1:def 4;
dom (ProjMap2 ((F2 - F1),d)) = ((dom (ProjMap2 (F2,d))) /\ (dom (ProjMap2 (F1,d)))) \ ((((ProjMap2 (F2,d)) " {+infty}) /\ ((ProjMap2 (F1,d)) " {+infty})) \/ (((ProjMap2 (F2,d)) " {-infty}) /\ ((ProjMap2 (F1,d)) " {-infty}))) by A2, B1;
then A6: dom (ProjMap2 ((F2 - F1),d)) = dom ((ProjMap2 (F2,d)) - (ProjMap2 (F1,d))) by MESFUNC1:def 4;
for c being object st c in dom (ProjMap2 ((F1 - F2),d)) holds
(ProjMap2 ((F1 - F2),d)) . c = ((ProjMap2 (F1,d)) - (ProjMap2 (F2,d))) . c

proof

let c be object ; :: thesis: ( c in dom (ProjMap2 ((F1 - F2),d)) implies (ProjMap2 ((F1 - F2),d)) . c = ((ProjMap2 (F1,d)) - (ProjMap2 (F2,d))) . c )
assume A3: c in dom (ProjMap2 ((F1 - F2),d)) ; :: thesis: (ProjMap2 ((F1 - F2),d)) . c = ((ProjMap2 (F1,d)) - (ProjMap2 (F2,d))) . c
then A4: ( (ProjMap2 ((F1 - F2),d)) . c = (F1 - F2) . (c,d) & (ProjMap2 (F1,d)) . c = F1 . (c,d) & (ProjMap2 (F2,d)) . c = F2 . (c,d) ) by MESFUNC9:def 7;
reconsider c1 = c as Element of C by A3;
[c,d] in [:C,D:] by A3, ZFMISC_1:def 2;
then (ProjMap2 ((F1 - F2),d)) . c = ((ProjMap2 (F1,d)) . c) - ((ProjMap2 (F2,d)) . c) by A4, Th7;
hence (ProjMap2 ((F1 - F2),d)) . c = ((ProjMap2 (F1,d)) - (ProjMap2 (F2,d))) . c by A3, A5, MESFUNC1:def 4; :: thesis: verum

end;

hence ProjMap2 ((F1 - F2),d) = (ProjMap2 (F1,d)) - (ProjMap2 (F2,d)) by A5, FUNCT_1:2; :: thesis: ProjMap2 ((F2 - F1),d) = (ProjMap2 (F2,d)) - (ProjMap2 (F1,d))
for c being object st c in dom (ProjMap2 ((F2 - F1),d)) holds
(ProjMap2 ((F2 - F1),d)) . c = ((ProjMap2 (F2,d)) - (ProjMap2 (F1,d))) . c

proof

let c be object ; :: thesis: ( c in dom (ProjMap2 ((F2 - F1),d)) implies (ProjMap2 ((F2 - F1),d)) . c = ((ProjMap2 (F2,d)) - (ProjMap2 (F1,d))) . c )
assume A3: c in dom (ProjMap2 ((F2 - F1),d)) ; :: thesis: (ProjMap2 ((F2 - F1),d)) . c = ((ProjMap2 (F2,d)) - (ProjMap2 (F1,d))) . c
then A4: ( (ProjMap2 ((F2 - F1),d)) . c = (F2 - F1) . (c,d) & (ProjMap2 (F1,d)) . c = F1 . (c,d) & (ProjMap2 (F2,d)) . c = F2 . (c,d) ) by MESFUNC9:def 7;
reconsider c1 = c as Element of C by A3;
[c,d] in [:C,D:] by A3, ZFMISC_1:def 2;
then (ProjMap2 ((F2 - F1),d)) . c = ((ProjMap2 (F2,d)) . c) - ((ProjMap2 (F1,d)) . c) by A4, Th7;
hence (ProjMap2 ((F2 - F1),d)) . c = ((ProjMap2 (F2,d)) - (ProjMap2 (F1,d))) . c by A3, A6, MESFUNC1:def 4; :: thesis: verum

end;

hence ProjMap2 ((F2 - F1),d) = (ProjMap2 (F2,d)) - (ProjMap2 (F1,d)) by A6, FUNCT_1:2; :: thesis: verum