let X1, X2 be non empty set ; for Y being set
for f being PartFunc of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 holds
( ( x in dom (ProjPMap2 (f,y)) implies (ProjPMap2 (f,y)) . x = f . (x,y) ) & ( y in dom (ProjPMap1 (f,x)) implies (ProjPMap1 (f,x)) . y = f . (x,y) ) )
let Y be set ; for f being PartFunc of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 holds
( ( x in dom (ProjPMap2 (f,y)) implies (ProjPMap2 (f,y)) . x = f . (x,y) ) & ( y in dom (ProjPMap1 (f,x)) implies (ProjPMap1 (f,x)) . y = f . (x,y) ) )
let f be PartFunc of [:X1,X2:],Y; for x being Element of X1
for y being Element of X2 holds
( ( x in dom (ProjPMap2 (f,y)) implies (ProjPMap2 (f,y)) . x = f . (x,y) ) & ( y in dom (ProjPMap1 (f,x)) implies (ProjPMap1 (f,x)) . y = f . (x,y) ) )
let c be Element of X1; for y being Element of X2 holds
( ( c in dom (ProjPMap2 (f,y)) implies (ProjPMap2 (f,y)) . c = f . (c,y) ) & ( y in dom (ProjPMap1 (f,c)) implies (ProjPMap1 (f,c)) . y = f . (c,y) ) )
let d be Element of X2; ( ( c in dom (ProjPMap2 (f,d)) implies (ProjPMap2 (f,d)) . c = f . (c,d) ) & ( d in dom (ProjPMap1 (f,c)) implies (ProjPMap1 (f,c)) . d = f . (c,d) ) )
assume
d in dom (ProjPMap1 (f,c))
; (ProjPMap1 (f,c)) . d = f . (c,d)
then
d in X-section ((dom f),c)
by Def3;
then
d in { y where y is Element of X2 : [c,y] in dom f }
by MEASUR11:def 4;
then
ex y being Element of X2 st
( d = y & [c,y] in dom f )
;
hence
(ProjPMap1 (f,c)) . d = f . (c,d)
by Def3; verum