let X, Y, Z be non empty set ; :: thesis: for A being Subset of X
for B being Subset of Y
for y being Element of Y
for f being PartFunc of [:X,Y:],Z st dom f = [:A,B:] holds
( ( y in B implies dom (ProjPMap2 (f,y)) = A ) & ( not y in B implies dom (ProjPMap2 (f,y)) = {} ) )
let A be Subset of X; :: thesis: for B being Subset of Y
for y being Element of Y
for f being PartFunc of [:X,Y:],Z st dom f = [:A,B:] holds
( ( y in B implies dom (ProjPMap2 (f,y)) = A ) & ( not y in B implies dom (ProjPMap2 (f,y)) = {} ) )
let B be Subset of Y; :: thesis: for y being Element of Y
for f being PartFunc of [:X,Y:],Z st dom f = [:A,B:] holds
( ( y in B implies dom (ProjPMap2 (f,y)) = A ) & ( not y in B implies dom (ProjPMap2 (f,y)) = {} ) )
let y be Element of Y; :: thesis: for f being PartFunc of [:X,Y:],Z st dom f = [:A,B:] holds
( ( y in B implies dom (ProjPMap2 (f,y)) = A ) & ( not y in B implies dom (ProjPMap2 (f,y)) = {} ) )
let f be PartFunc of [:X,Y:],Z; :: thesis: ( dom f = [:A,B:] implies ( ( y in B implies dom (ProjPMap2 (f,y)) = A ) & ( not y in B implies dom (ProjPMap2 (f,y)) = {} ) ) )
assume A1: dom f = [:A,B:] ; :: thesis: ( ( y in B implies dom (ProjPMap2 (f,y)) = A ) & ( not y in B implies dom (ProjPMap2 (f,y)) = {} ) )

hereby :: thesis: ( not y in B implies dom (ProjPMap2 (f,y)) = {} )

assume A2: y in B ; :: thesis: dom (ProjPMap2 (f,y)) = A
for x being Element of X holds
( x in Y-section ((dom f),y) iff x in A )

proof

let x be Element of X; :: thesis: ( x in Y-section ((dom f),y) iff x in A )

hereby :: thesis: ( x in A implies x in Y-section ((dom f),y) )

assume x in Y-section ((dom f),y) ; :: thesis: x in A
then [x,y] in dom f by MESFUN12:25;
hence x in A by A1, ZFMISC_1:87; :: thesis: verum

end;

assume x in A ; :: thesis: x in Y-section ((dom f),y)
then [x,y] in dom f by A1, A2, ZFMISC_1:87;
then x in { x where x is Element of X : [x,y] in dom f } ;
hence x in Y-section ((dom f),y) by MEASUR11:def 5; :: thesis: verum

end;

then Y-section ((dom f),y) = A by SUBSET_1:3;
hence dom (ProjPMap2 (f,y)) = A by MESFUN12:def 4; :: thesis: verum

end;

assume A3: not y in B ; :: thesis: dom (ProjPMap2 (f,y)) = {}

now :: thesis: not Y-section ((dom f),y) <> {}

assume Y-section ((dom f),y) <> {} ; :: thesis: contradiction
then consider x being object such that
A4: x in Y-section ((dom f),y) by XBOOLE_0:def 1;
reconsider x = x as Element of X by A4;
[x,y] in dom f by A4, MESFUN12:25;
hence contradiction by A1, A3, ZFMISC_1:87; :: thesis: verum

end;

hence dom (ProjPMap2 (f,y)) = {} by MESFUN12:def 4; :: thesis: verum