let X, Y be non empty set ; :: thesis: for A, Z being set
for f being PartFunc of [:X,Y:],Z
for y being Element of Y holds Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A
let A, Z be set ; :: thesis: for f being PartFunc of [:X,Y:],Z
for y being Element of Y holds Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A
let f be PartFunc of [:X,Y:],Z; :: thesis: for y being Element of Y holds Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A
let y be Element of Y; :: thesis: Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A
reconsider E = f " A as Subset of [:X,Y:] ;

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
A1: ( x1 = x & [x1,y] in E ) ;
A2: ( [x,y] in dom f & f . [x,y] in A ) by A1, FUNCT_1:def 7;
then x in { x where x is Element of X : [x,y] in dom f } by A1;
then x in Y-section ((dom f),y) by MEASUR11:def 5;
then A3: x in dom (ProjPMap2 (f,y)) by Def4;
(ProjPMap2 (f,y)) . x1 = f . (x1,y) by A1, A2, Def4;
hence x in (ProjPMap2 (f,y)) " A by A1, A2, A3, FUNCT_1:def 7; :: thesis: verum

end;

then A4: 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 A5: ( 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
A6: ( x1 = x & [x1,y] in dom f ) ;
f . (x1,y) in A by A5, A6, Def4;
then [x1,y] in f " A by A6, FUNCT_1:def 7;
then x in { x where x is Element of X : [x,y] in f " A } by A6;
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 A4; :: thesis: verum