let X1, X2, Y be non empty set ; for f being Function of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 (f,x) = ProjMap1 (f,x) & ProjPMap2 (f,y) = ProjMap2 (f,y) )
let f be Function of [:X1,X2:],Y; for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 (f,x) = ProjMap1 (f,x) & ProjPMap2 (f,y) = ProjMap2 (f,y) )
let x be Element of X1; for y being Element of X2 holds
( ProjPMap1 (f,x) = ProjMap1 (f,x) & ProjPMap2 (f,y) = ProjMap2 (f,y) )
let y be Element of X2; ( ProjPMap1 (f,x) = ProjMap1 (f,x) & ProjPMap2 (f,y) = ProjMap2 (f,y) )
dom f = [:X1,X2:]
by FUNCT_2:def 1;
then A1:
dom f = [#] [:X1,X2:]
by SUBSET_1:def 3;
then
X-section ((dom f),x) = X2
by MEASUR11:24;
then
dom (ProjPMap1 (f,x)) = X2
by Def3;
then A2:
dom (ProjPMap1 (f,x)) = dom (ProjMap1 (f,x))
by FUNCT_2:def 1;
for y being Element of X2 st y in dom (ProjPMap1 (f,x)) holds
(ProjPMap1 (f,x)) . y = (ProjMap1 (f,x)) . y
proof
let y be
Element of
X2;
( y in dom (ProjPMap1 (f,x)) implies (ProjPMap1 (f,x)) . y = (ProjMap1 (f,x)) . y )
assume
y in dom (ProjPMap1 (f,x))
;
(ProjPMap1 (f,x)) . y = (ProjMap1 (f,x)) . y
then
(ProjPMap1 (f,x)) . y = f . (
x,
y)
by Th26;
hence
(ProjPMap1 (f,x)) . y = (ProjMap1 (f,x)) . y
by MESFUNC9:def 6;
verum
end;
hence
ProjPMap1 (f,x) = ProjMap1 (f,x)
by A2, PARTFUN1:5; ProjPMap2 (f,y) = ProjMap2 (f,y)
Y-section ((dom f),y) = X1
by A1, MEASUR11:24;
then
dom (ProjPMap2 (f,y)) = X1
by Def4;
then A3:
dom (ProjPMap2 (f,y)) = dom (ProjMap2 (f,y))
by FUNCT_2:def 1;
for x being Element of X1 st x in dom (ProjPMap2 (f,y)) holds
(ProjPMap2 (f,y)) . x = (ProjMap2 (f,y)) . x
proof
let x be
Element of
X1;
( x in dom (ProjPMap2 (f,y)) implies (ProjPMap2 (f,y)) . x = (ProjMap2 (f,y)) . x )
assume
x in dom (ProjPMap2 (f,y))
;
(ProjPMap2 (f,y)) . x = (ProjMap2 (f,y)) . x
then
(ProjPMap2 (f,y)) . x = f . (
x,
y)
by Th26;
hence
(ProjPMap2 (f,y)) . x = (ProjMap2 (f,y)) . x
by MESFUNC9:def 7;
verum
end;
hence
ProjPMap2 (f,y) = ProjMap2 (f,y)
by A3, PARTFUN1:5; verum