let X1, X2 be non empty set ; for x being Element of X1
for y being Element of X2
for r being Real
for f being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x)) & ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y)) )
let x be Element of X1; for y being Element of X2
for r being Real
for f being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x)) & ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y)) )
let y be Element of X2; for r being Real
for f being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x)) & ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y)) )
let r be Real; for f being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x)) & ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y)) )
let f be PartFunc of [:X1,X2:],ExtREAL; ( ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x)) & ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y)) )
( dom (ProjPMap1 ((r (#) f),x)) = X-section ((dom (r (#) f)),x) & dom (ProjPMap2 ((r (#) f),y)) = Y-section ((dom (r (#) f)),y) )
by Def3, Def4;
then A1:
( dom (ProjPMap1 ((r (#) f),x)) = X-section ((dom f),x) & dom (ProjPMap2 ((r (#) f),y)) = Y-section ((dom f),y) )
by MESFUNC1:def 6;
( dom (r (#) (ProjPMap1 (f,x))) = dom (ProjPMap1 (f,x)) & dom (r (#) (ProjPMap2 (f,y))) = dom (ProjPMap2 (f,y)) )
by MESFUNC1:def 6;
then A2:
( dom (r (#) (ProjPMap1 (f,x))) = X-section ((dom f),x) & dom (r (#) (ProjPMap2 (f,y))) = Y-section ((dom f),y) )
by Def3, Def4;
now for y being Element of X2 st y in dom (ProjPMap1 ((r (#) f),x)) holds
(ProjPMap1 ((r (#) f),x)) . y = (r (#) (ProjPMap1 (f,x))) . ylet y be
Element of
X2;
( y in dom (ProjPMap1 ((r (#) f),x)) implies (ProjPMap1 ((r (#) f),x)) . y = (r (#) (ProjPMap1 (f,x))) . y )assume A3:
y in dom (ProjPMap1 ((r (#) f),x))
;
(ProjPMap1 ((r (#) f),x)) . y = (r (#) (ProjPMap1 (f,x))) . ythen
y in { y where y is Element of X2 : [x,y] in dom f }
by A1, MEASUR11:def 4;
then A4:
ex
y1 being
Element of
X2 st
(
y1 = y &
[x,y1] in dom f )
;
then A5:
[x,y] in dom (r (#) f)
by MESFUNC1:def 6;
A6:
f . (
x,
y)
= f . [x,y]
;
(r (#) (ProjPMap1 (f,x))) . y =
r * ((ProjPMap1 (f,x)) . y)
by A1, A2, A3, MESFUNC1:def 6
.=
r * (f . [x,y])
by A4, A6, Def3
.=
(r (#) f) . (
x,
y)
by A5, MESFUNC1:def 6
;
hence
(ProjPMap1 ((r (#) f),x)) . y = (r (#) (ProjPMap1 (f,x))) . y
by A5, Def3;
verum end;
hence
ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x))
by A1, A2, PARTFUN1:5; ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y))
now for x being Element of X1 st x in dom (ProjPMap2 ((r (#) f),y)) holds
(ProjPMap2 ((r (#) f),y)) . x = (r (#) (ProjPMap2 (f,y))) . xlet x be
Element of
X1;
( x in dom (ProjPMap2 ((r (#) f),y)) implies (ProjPMap2 ((r (#) f),y)) . x = (r (#) (ProjPMap2 (f,y))) . x )assume A7:
x in dom (ProjPMap2 ((r (#) f),y))
;
(ProjPMap2 ((r (#) f),y)) . x = (r (#) (ProjPMap2 (f,y))) . xthen
x in { x where x is Element of X1 : [x,y] in dom f }
by A1, MEASUR11:def 5;
then A8:
ex
x1 being
Element of
X1 st
(
x1 = x &
[x1,y] in dom f )
;
then A9:
[x,y] in dom (r (#) f)
by MESFUNC1:def 6;
A10:
f . (
x,
y)
= f . [x,y]
;
(r (#) (ProjPMap2 (f,y))) . x =
r * ((ProjPMap2 (f,y)) . x)
by A1, A2, A7, MESFUNC1:def 6
.=
r * (f . [x,y])
by A8, A10, Def4
.=
(r (#) f) . (
x,
y)
by A9, MESFUNC1:def 6
;
hence
(ProjPMap2 ((r (#) f),y)) . x = (r (#) (ProjPMap2 (f,y))) . x
by A9, Def4;
verum end;
hence
ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y))
by A1, A2, PARTFUN1:5; verum