let X, Y be non empty set ; :: thesis: for f being PartFunc of [:X,Y:],REAL
for x being Element of X
for y being Element of Y holds
( ProjPMap1 ((R_EAL f),x) is PartFunc of Y,REAL & ProjPMap1 (|.(R_EAL f).|,x) is PartFunc of Y,REAL & ProjPMap2 ((R_EAL f),y) is PartFunc of X,REAL & ProjPMap2 (|.(R_EAL f).|,y) is PartFunc of X,REAL )
let f be PartFunc of [:X,Y:],REAL; :: thesis: for x being Element of X
for y being Element of Y holds
( ProjPMap1 ((R_EAL f),x) is PartFunc of Y,REAL & ProjPMap1 (|.(R_EAL f).|,x) is PartFunc of Y,REAL & ProjPMap2 ((R_EAL f),y) is PartFunc of X,REAL & ProjPMap2 (|.(R_EAL f).|,y) is PartFunc of X,REAL )
let x be Element of X; :: thesis: for y being Element of Y holds
( ProjPMap1 ((R_EAL f),x) is PartFunc of Y,REAL & ProjPMap1 (|.(R_EAL f).|,x) is PartFunc of Y,REAL & ProjPMap2 ((R_EAL f),y) is PartFunc of X,REAL & ProjPMap2 (|.(R_EAL f).|,y) is PartFunc of X,REAL )
let y be Element of Y; :: thesis: ( ProjPMap1 ((R_EAL f),x) is PartFunc of Y,REAL & ProjPMap1 (|.(R_EAL f).|,x) is PartFunc of Y,REAL & ProjPMap2 ((R_EAL f),y) is PartFunc of X,REAL & ProjPMap2 (|.(R_EAL f).|,y) is PartFunc of X,REAL )
rng (ProjPMap1 ((R_EAL f),x)) c= rng (R_EAL f) by Th29;
then rng (ProjPMap1 ((R_EAL f),x)) c= rng f by MESFUNC5:def 7;
hence ProjPMap1 ((R_EAL f),x) is PartFunc of Y,REAL by RELSET_1:6, XBOOLE_1:1; :: thesis: ( ProjPMap1 (|.(R_EAL f).|,x) is PartFunc of Y,REAL & ProjPMap2 ((R_EAL f),y) is PartFunc of X,REAL & ProjPMap2 (|.(R_EAL f).|,y) is PartFunc of X,REAL )
rng (ProjPMap1 (|.(R_EAL f).|,x)) c= rng |.(R_EAL f).| by Th29;
then rng (ProjPMap1 (|.(R_EAL f).|,x)) c= rng (R_EAL (abs f)) by MESFUNC6:1;
then rng (ProjPMap1 (|.(R_EAL f).|,x)) c= rng (abs f) by MESFUNC5:def 7;
hence ProjPMap1 (|.(R_EAL f).|,x) is PartFunc of Y,REAL by RELSET_1:6, XBOOLE_1:1; :: thesis: ( ProjPMap2 ((R_EAL f),y) is PartFunc of X,REAL & ProjPMap2 (|.(R_EAL f).|,y) is PartFunc of X,REAL )
rng (ProjPMap2 ((R_EAL f),y)) c= rng (R_EAL f) by Th29;
then rng (ProjPMap2 ((R_EAL f),y)) c= rng f by MESFUNC5:def 7;
hence ProjPMap2 ((R_EAL f),y) is PartFunc of X,REAL by RELSET_1:6, XBOOLE_1:1; :: thesis: ProjPMap2 (|.(R_EAL f).|,y) is PartFunc of X,REAL
rng (ProjPMap2 (|.(R_EAL f).|,y)) c= rng |.(R_EAL f).| by Th29;
then rng (ProjPMap2 (|.(R_EAL f).|,y)) c= rng (R_EAL (abs f)) by MESFUNC6:1;
then rng (ProjPMap2 (|.(R_EAL f).|,y)) c= rng (abs f) by MESFUNC5:def 7;
hence ProjPMap2 (|.(R_EAL f).|,y) is PartFunc of X,REAL by RELSET_1:6, XBOOLE_1:1; :: thesis: verum