let X, Y be non empty set ; :: thesis: for Z being set
for f being PartFunc of [:X,Y:],Z
for x being Element of X
for y being Element of Y holds
( rng (ProjPMap1 (f,x)) c= rng f & rng (ProjPMap2 (f,y)) c= rng f )
let Z be set ; :: thesis: for f being PartFunc of [:X,Y:],Z
for x being Element of X
for y being Element of Y holds
( rng (ProjPMap1 (f,x)) c= rng f & rng (ProjPMap2 (f,y)) c= rng f )
let f be PartFunc of [:X,Y:],Z; :: thesis: for x being Element of X
for y being Element of Y holds
( rng (ProjPMap1 (f,x)) c= rng f & rng (ProjPMap2 (f,y)) c= rng f )
let x be Element of X; :: thesis: for y being Element of Y holds
( rng (ProjPMap1 (f,x)) c= rng f & rng (ProjPMap2 (f,y)) c= rng f )
let y be Element of Y; :: thesis: ( rng (ProjPMap1 (f,x)) c= rng f & rng (ProjPMap2 (f,y)) c= rng f )

now :: thesis: for z being Element of Z st z in rng (ProjPMap1 (f,x)) holds
z in rng f

let z be Element of Z; :: thesis: ( z in rng (ProjPMap1 (f,x)) implies z in rng f )
assume z in rng (ProjPMap1 (f,x)) ; :: thesis: z in rng f
then consider y being Element of Y such that
A1: ( y in dom (ProjPMap1 (f,x)) & z = (ProjPMap1 (f,x)) . y ) by PARTFUN1:3;
y in X-section ((dom f),x) by A1, MESFUN12:def 3;
then y in { y where y is Element of Y : [x,y] in dom f } by MEASUR11:def 4;
then A2: ex y2 being Element of Y st
( y2 = y & [x,y2] in dom f ) ;
then z = f . (x,y) by A1, MESFUN12:def 3;
hence z in rng f by A2, FUNCT_1:3; :: thesis: verum

end;

hence rng (ProjPMap1 (f,x)) c= rng f ; :: thesis: rng (ProjPMap2 (f,y)) c= rng f

now :: thesis: for z being Element of Z st z in rng (ProjPMap2 (f,y)) holds
z in rng f

let z be Element of Z; :: thesis: ( z in rng (ProjPMap2 (f,y)) implies z in rng f )
assume z in rng (ProjPMap2 (f,y)) ; :: thesis: z in rng f
then consider x being Element of X such that
A3: ( x in dom (ProjPMap2 (f,y)) & z = (ProjPMap2 (f,y)) . x ) by PARTFUN1:3;
x in Y-section ((dom f),y) by A3, MESFUN12:def 4;
then x in { x where x is Element of X : [x,y] in dom f } by MEASUR11:def 5;
then A4: ex x2 being Element of X st
( x2 = x & [x2,y] in dom f ) ;
then z = f . (x,y) by A3, MESFUN12:def 4;
hence z in rng f by A4, FUNCT_1:3; :: thesis: verum

end;

hence rng (ProjPMap2 (f,y)) c= rng f ; :: thesis: verum