let X, Y be non empty set ; :: thesis: 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 ; :: thesis: 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; :: thesis: for x being Element of X holds X-section ((f " A),x) = (ProjPMap1 (f,x)) " A
let x be Element of X; :: thesis: X-section ((f " A),x) = (ProjPMap1 (f,x)) " A
reconsider E = f " A as Subset of [:X,Y:] ;

now :: thesis: for y being object st y in X-section ((f " A),x) holds
y in (ProjPMap1 (f,x)) " A

let y be object ; :: thesis: ( y in X-section ((f " A),x) implies y in (ProjPMap1 (f,x)) " A )
assume y in X-section ((f " A),x) ; :: thesis: y in (ProjPMap1 (f,x)) " A
then 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; :: thesis: verum

end;

then A4: X-section ((f " A),x) c= (ProjPMap1 (f,x)) " A ;

now :: thesis: for y being object st y in (ProjPMap1 (f,x)) " A holds
y in X-section ((f " A),x)

let y be object ; :: thesis: ( y in (ProjPMap1 (f,x)) " A implies y in X-section ((f " A),x) )
assume y in (ProjPMap1 (f,x)) " A ; :: thesis: 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; :: thesis: 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; :: thesis: verum