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

hereby :: thesis: ( not x in A implies dom (ProjPMap1 (f,x)) = {} )

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

proof

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

hereby :: thesis: ( y in B implies y in X-section ((dom f),x) )

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

end;

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

end;

then X-section ((dom f),x) = B by SUBSET_1:3;
hence dom (ProjPMap1 (f,x)) = B by MESFUN12:def 3; :: thesis: verum

end;

assume A3: not x in A ; :: thesis: dom (ProjPMap1 (f,x)) = {}

now :: thesis: not X-section ((dom f),x) <> {}

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

end;

hence dom (ProjPMap1 (f,x)) = {} by MESFUN12:def 3; :: thesis: verum