let X1, X2 be non empty set ; for f being PartFunc of [:X1,X2:],ExtREAL
for y being Element of X2 holds
( ProjPMap2 ((max+ f),y) = max+ (ProjPMap2 (f,y)) & ProjPMap2 ((max- f),y) = max- (ProjPMap2 (f,y)) )
let f be PartFunc of [:X1,X2:],ExtREAL; for y being Element of X2 holds
( ProjPMap2 ((max+ f),y) = max+ (ProjPMap2 (f,y)) & ProjPMap2 ((max- f),y) = max- (ProjPMap2 (f,y)) )
let y be Element of X2; ( ProjPMap2 ((max+ f),y) = max+ (ProjPMap2 (f,y)) & ProjPMap2 ((max- f),y) = max- (ProjPMap2 (f,y)) )
( dom (ProjPMap2 ((max+ f),y)) = Y-section ((dom (max+ f)),y) & dom (ProjPMap2 ((max- f),y)) = Y-section ((dom (max- f)),y) )
by Def4;
then A1:
( dom (ProjPMap2 ((max+ f),y)) = Y-section ((dom f),y) & dom (ProjPMap2 ((max- f),y)) = Y-section ((dom f),y) )
by MESFUNC2:def 2, MESFUNC2:def 3;
( dom (max+ (ProjPMap2 (f,y))) = dom (ProjPMap2 (f,y)) & dom (max- (ProjPMap2 (f,y))) = dom (ProjPMap2 (f,y)) )
by MESFUNC2:def 2, MESFUNC2:def 3;
then A2:
( dom (max+ (ProjPMap2 (f,y))) = Y-section ((dom f),y) & dom (max- (ProjPMap2 (f,y))) = Y-section ((dom f),y) )
by Def4;
for x being Element of X1 st x in dom (ProjPMap2 ((max+ f),y)) holds
(ProjPMap2 ((max+ f),y)) . x = (max+ (ProjPMap2 (f,y))) . x
proof
let x be
Element of
X1;
( x in dom (ProjPMap2 ((max+ f),y)) implies (ProjPMap2 ((max+ f),y)) . x = (max+ (ProjPMap2 (f,y))) . x )
assume A3:
x in dom (ProjPMap2 ((max+ f),y))
;
(ProjPMap2 ((max+ f),y)) . x = (max+ (ProjPMap2 (f,y))) . x
then
x in { x where x is Element of X1 : [x,y] in dom f }
by A1, MEASUR11:def 5;
then A4:
ex
x1 being
Element of
X1 st
(
x1 = x &
[x1,y] in dom f )
;
set z =
[x,y];
A5:
[x,y] in dom (max+ f)
by A4, MESFUNC2:def 2;
then A6:
(ProjPMap2 ((max+ f),y)) . x =
(max+ f) . (
x,
y)
by Def4
.=
max (
(f . [x,y]),
0)
by A5, MESFUNC2:def 2
;
(ProjPMap2 (f,y)) . x = f . (
x,
y)
by A4, Def4;
hence
(ProjPMap2 ((max+ f),y)) . x = (max+ (ProjPMap2 (f,y))) . x
by A6, A1, A3, A2, MESFUNC2:def 2;
verum
end;
hence
ProjPMap2 ((max+ f),y) = max+ (ProjPMap2 (f,y))
by A1, A2, PARTFUN1:5; ProjPMap2 ((max- f),y) = max- (ProjPMap2 (f,y))
for x being Element of X1 st x in dom (ProjPMap2 ((max- f),y)) holds
(ProjPMap2 ((max- f),y)) . x = (max- (ProjPMap2 (f,y))) . x
proof
let x be
Element of
X1;
( x in dom (ProjPMap2 ((max- f),y)) implies (ProjPMap2 ((max- f),y)) . x = (max- (ProjPMap2 (f,y))) . x )
assume A8:
x in dom (ProjPMap2 ((max- f),y))
;
(ProjPMap2 ((max- f),y)) . x = (max- (ProjPMap2 (f,y))) . x
then
x in { x where x is Element of X1 : [x,y] in dom f }
by A1, MEASUR11:def 5;
then A9:
ex
x1 being
Element of
X1 st
(
x1 = x &
[x1,y] in dom f )
;
set z =
[x,y];
A10:
[x,y] in dom (max- f)
by A9, MESFUNC2:def 3;
then A11:
(ProjPMap2 ((max- f),y)) . x =
(max- f) . (
x,
y)
by Def4
.=
max (
(- (f . [x,y])),
0)
by A10, MESFUNC2:def 3
;
(ProjPMap2 (f,y)) . x = f . (
x,
y)
by A9, Def4;
hence
(ProjPMap2 ((max- f),y)) . x = (max- (ProjPMap2 (f,y))) . x
by A11, A1, A8, A2, MESFUNC2:def 3;
verum
end;
hence
ProjPMap2 ((max- f),y) = max- (ProjPMap2 (f,y))
by A1, A2, PARTFUN1:5; verum