let X, Y be non empty set ; for A, Z being set
for f being PartFunc of [:X,Y:],Z
for x being Element of X holds X-section ((f " A),x) = (ProjPMap1 (f,x)) " A
let A, Z be set ; for f being PartFunc of [:X,Y:],Z
for x being Element of X holds X-section ((f " A),x) = (ProjPMap1 (f,x)) " A
let f be PartFunc of [:X,Y:],Z; for x being Element of X holds X-section ((f " A),x) = (ProjPMap1 (f,x)) " A
let x be Element of X; X-section ((f " A),x) = (ProjPMap1 (f,x)) " A
reconsider E = f " A as Subset of [:X,Y:] ;
now for y being object st y in X-section ((f " A),x) holds
y in (ProjPMap1 (f,x)) " Alet y be
object ;
( y in X-section ((f " A),x) implies y in (ProjPMap1 (f,x)) " A )assume
y in X-section (
(f " A),
x)
;
y in (ProjPMap1 (f,x)) " Athen
y in { y where y is Element of Y : [x,y] in E }
by MEASUR11:def 4;
then consider y1 being
Element of
Y such that A1:
(
y1 = y &
[x,y1] in E )
;
A2:
(
[x,y] in dom f &
f . [x,y] in A )
by A1, FUNCT_1:def 7;
then
y in { y where y is Element of Y : [x,y] in dom f }
by A1;
then
y in X-section (
(dom f),
x)
by MEASUR11:def 4;
then A3:
y in dom (ProjPMap1 (f,x))
by Def3;
(ProjPMap1 (f,x)) . y1 = f . (
x,
y1)
by A1, A2, Def3;
hence
y in (ProjPMap1 (f,x)) " A
by A1, A2, A3, FUNCT_1:def 7;
verum end;
then A4:
X-section ((f " A),x) c= (ProjPMap1 (f,x)) " A
;
now for y being object st y in (ProjPMap1 (f,x)) " A holds
y in X-section ((f " A),x)let y be
object ;
( y in (ProjPMap1 (f,x)) " A implies y in X-section ((f " A),x) )assume
y in (ProjPMap1 (f,x)) " A
;
y in X-section ((f " A),x)then A5:
(
y in dom (ProjPMap1 (f,x)) &
(ProjPMap1 (f,x)) . y in A )
by FUNCT_1:def 7;
then
y in X-section (
(dom f),
x)
by Def3;
then
y in { y where y is Element of Y : [x,y] in dom f }
by MEASUR11:def 4;
then consider y1 being
Element of
Y such that A6:
(
y1 = y &
[x,y1] in dom f )
;
f . (
x,
y1)
in A
by A5, A6, Def3;
then
[x,y1] in f " A
by A6, FUNCT_1:def 7;
then
y in { y where y is Element of Y : [x,y] in f " A }
by A6;
hence
y in X-section (
(f " A),
x)
by MEASUR11:def 4;
verum end;
then
(ProjPMap1 (f,x)) " A c= X-section ((f " A),x)
;
hence
X-section ((f " A),x) = (ProjPMap1 (f,x)) " A
by A4; verum