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

proof

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

end;

hence ProjMap1 ((F1 + F2),c) = (ProjMap1 (F1,c)) + (ProjMap1 (F2,c)) by A5, FUNCT_1:2; :: thesis: verum