let C, D be non empty set ; for F1 being without-infty Function of [:C,D:],ExtREAL
for F2 being without+infty Function of [:C,D:],ExtREAL
for c being Element of C holds
( ProjMap1 ((F1 - F2),c) = (ProjMap1 (F1,c)) - (ProjMap1 (F2,c)) & ProjMap1 ((F2 - F1),c) = (ProjMap1 (F2,c)) - (ProjMap1 (F1,c)) )
let F1 be without-infty Function of [:C,D:],ExtREAL; for F2 being without+infty Function of [:C,D:],ExtREAL
for c being Element of C holds
( ProjMap1 ((F1 - F2),c) = (ProjMap1 (F1,c)) - (ProjMap1 (F2,c)) & ProjMap1 ((F2 - F1),c) = (ProjMap1 (F2,c)) - (ProjMap1 (F1,c)) )
let F2 be without+infty Function of [:C,D:],ExtREAL; for c being Element of C holds
( ProjMap1 ((F1 - F2),c) = (ProjMap1 (F1,c)) - (ProjMap1 (F2,c)) & ProjMap1 ((F2 - F1),c) = (ProjMap1 (F2,c)) - (ProjMap1 (F1,c)) )
let c be Element of C; ( ProjMap1 ((F1 - F2),c) = (ProjMap1 (F1,c)) - (ProjMap1 (F2,c)) & ProjMap1 ((F2 - F1),c) = (ProjMap1 (F2,c)) - (ProjMap1 (F1,c)) )
A2:
( dom (ProjMap1 ((F1 - F2),c)) = D & dom (ProjMap1 ((F2 - F1),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 3, MESFUNC5:def 4;
then B1:
( (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 4;
dom (ProjMap1 ((F2 - F1),c)) = ((dom (ProjMap1 (F2,c))) /\ (dom (ProjMap1 (F1,c)))) \ ((((ProjMap1 (F2,c)) " {+infty}) /\ ((ProjMap1 (F1,c)) " {+infty})) \/ (((ProjMap1 (F2,c)) " {-infty}) /\ ((ProjMap1 (F1,c)) " {-infty})))
by A2, B1;
then A6:
dom (ProjMap1 ((F2 - F1),c)) = dom ((ProjMap1 (F2,c)) - (ProjMap1 (F1,c)))
by MESFUNC1:def 4;
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 ;
( 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))
;
(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 4;
verum
end;
hence
ProjMap1 ((F1 - F2),c) = (ProjMap1 (F1,c)) - (ProjMap1 (F2,c))
by A5, FUNCT_1:2; ProjMap1 ((F2 - F1),c) = (ProjMap1 (F2,c)) - (ProjMap1 (F1,c))
for d being object st d in dom (ProjMap1 ((F2 - F1),c)) holds
(ProjMap1 ((F2 - F1),c)) . d = ((ProjMap1 (F2,c)) - (ProjMap1 (F1,c))) . d
proof
let d be
object ;
( d in dom (ProjMap1 ((F2 - F1),c)) implies (ProjMap1 ((F2 - F1),c)) . d = ((ProjMap1 (F2,c)) - (ProjMap1 (F1,c))) . d )
assume A3:
d in dom (ProjMap1 ((F2 - F1),c))
;
(ProjMap1 ((F2 - F1),c)) . d = ((ProjMap1 (F2,c)) - (ProjMap1 (F1,c))) . d
then A4:
(
(ProjMap1 ((F2 - F1),c)) . d = (F2 - F1) . (
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 ((F2 - F1),c)) . d = ((ProjMap1 (F2,c)) . d) - ((ProjMap1 (F1,c)) . d)
by A4, Th7;
hence
(ProjMap1 ((F2 - F1),c)) . d = ((ProjMap1 (F2,c)) - (ProjMap1 (F1,c))) . d
by A3, A6, MESFUNC1:def 4;
verum
end;
hence
ProjMap1 ((F2 - F1),c) = (ProjMap1 (F2,c)) - (ProjMap1 (F1,c))
by A6, FUNCT_1:2; verum