let C, D be non empty set ; for F1, 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))
let F1, F2 be V184() Function of [:C,D:],ExtREAL; for d being Element of D holds ProjMap2 ((F1 + F2),d) = (ProjMap2 (F1,d)) + (ProjMap2 (F2,d))
let d be Element of D; ProjMap2 ((F1 + F2),d) = (ProjMap2 (F1,d)) + (ProjMap2 (F2,d))
A2:
( dom (ProjMap2 ((F1 + F2),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 4;
then
( (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 3;
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 ;
( 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))
;
(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 3;
verum
end;
hence
ProjMap2 ((F1 + F2),d) = (ProjMap2 (F1,d)) + (ProjMap2 (F2,d))
by A5, FUNCT_1:2; verum