let X, Y, Z be non empty set ; :: thesis: for f being PartFunc of [:X,Y:],Z
for x being Element of X
for y being Element of Y
for A being set holds
( X-section ((f " A),x) = (ProjPMap1 (f,x)) " A & Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A )
let f be PartFunc of [:X,Y:],Z; :: thesis: for x being Element of X
for y being Element of Y
for A being set holds
( X-section ((f " A),x) = (ProjPMap1 (f,x)) " A & Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A )
let x be Element of X; :: thesis: for y being Element of Y
for A being set holds
( X-section ((f " A),x) = (ProjPMap1 (f,x)) " A & Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A )
let y be Element of Y; :: thesis: for A being set holds
( X-section ((f " A),x) = (ProjPMap1 (f,x)) " A & Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A )
let A be set ; :: thesis: ( X-section ((f " A),x) = (ProjPMap1 (f,x)) " A & Y-section ((f " A),y) = (ProjPMap2 (f,y)) " 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: Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A

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

let x be object ; :: thesis: ( x in Y-section ((f " A),y) implies x in (ProjPMap2 (f,y)) " A )
assume x in Y-section ((f " A),y) ; :: thesis: x in (ProjPMap2 (f,y)) " A
then x in { x where x is Element of X : [x,y] in E } by MEASUR11:def 5;
then consider x1 being Element of X such that
A7: ( x1 = x & [x1,y] in E ) ;
A8: ( [x,y] in dom f & f . [x,y] in A ) by A7, FUNCT_1:def 7;
then x in { x where x is Element of X : [x,y] in dom f } by A7;
then x in Y-section ((dom f),y) by MEASUR11:def 5;
then A9: x in dom (ProjPMap2 (f,y)) by Def4;
(ProjPMap2 (f,y)) . x1 = f . (x1,y) by A7, A8, Def4;
hence x in (ProjPMap2 (f,y)) " A by A7, A8, A9, FUNCT_1:def 7; :: thesis: verum

end;

then A10: Y-section ((f " A),y) c= (ProjPMap2 (f,y)) " A ;

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

let x be object ; :: thesis: ( x in (ProjPMap2 (f,y)) " A implies x in Y-section ((f " A),y) )
assume x in (ProjPMap2 (f,y)) " A ; :: thesis: x in Y-section ((f " A),y)
then A11: ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x in A ) by FUNCT_1:def 7;
then x in Y-section ((dom f),y) by Def4;
then x in { x where x is Element of X : [x,y] in dom f } by MEASUR11:def 5;
then consider x1 being Element of X such that
A12: ( x1 = x & [x1,y] in dom f ) ;
f . (x1,y) in A by A11, A12, Def4;
then [x1,y] in f " A by A12, FUNCT_1:def 7;
then x in { x where x is Element of X : [x,y] in f " A } by A12;
hence x in Y-section ((f " A),y) by MEASUR11:def 5; :: thesis: verum

end;

then (ProjPMap2 (f,y)) " A c= Y-section ((f " A),y) ;
hence Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A by A10; :: thesis: verum