let X, Y 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:],REAL st dom f = [:A,B:] holds
( ( x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = B & dom (ProjPMap1 (|.(R_EAL f).|,x)) = B ) ) & ( not x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = {} & dom (ProjPMap1 (|.(R_EAL 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:],REAL st dom f = [:A,B:] holds
( ( x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = B & dom (ProjPMap1 (|.(R_EAL f).|,x)) = B ) ) & ( not x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = {} & dom (ProjPMap1 (|.(R_EAL f).|,x)) = {} ) ) )
let B be Subset of Y; :: thesis: for x being Element of X
for f being PartFunc of [:X,Y:],REAL st dom f = [:A,B:] holds
( ( x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = B & dom (ProjPMap1 (|.(R_EAL f).|,x)) = B ) ) & ( not x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = {} & dom (ProjPMap1 (|.(R_EAL f).|,x)) = {} ) ) )
let x be Element of X; :: thesis: for f being PartFunc of [:X,Y:],REAL st dom f = [:A,B:] holds
( ( x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = B & dom (ProjPMap1 (|.(R_EAL f).|,x)) = B ) ) & ( not x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = {} & dom (ProjPMap1 (|.(R_EAL f).|,x)) = {} ) ) )
let f be PartFunc of [:X,Y:],REAL; :: thesis: ( dom f = [:A,B:] implies ( ( x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = B & dom (ProjPMap1 (|.(R_EAL f).|,x)) = B ) ) & ( not x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = {} & dom (ProjPMap1 (|.(R_EAL f).|,x)) = {} ) ) ) )
assume dom f = [:A,B:] ; :: thesis: ( ( x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = B & dom (ProjPMap1 (|.(R_EAL f).|,x)) = B ) ) & ( not x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = {} & dom (ProjPMap1 (|.(R_EAL f).|,x)) = {} ) ) )
then A1: dom (R_EAL f) = [:A,B:] by MESFUNC5:def 7;
then A2: dom |.(R_EAL f).| = [:A,B:] by MESFUNC1:def 10;
hence ( x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = B & dom (ProjPMap1 (|.(R_EAL f).|,x)) = B ) ) by A1, Th25; :: thesis: ( not x in A implies ( dom (ProjPMap1 ((R_EAL f),x)) = {} & dom (ProjPMap1 (|.(R_EAL f).|,x)) = {} ) )
assume not x in A ; :: thesis: ( dom (ProjPMap1 ((R_EAL f),x)) = {} & dom (ProjPMap1 (|.(R_EAL f).|,x)) = {} )
hence ( dom (ProjPMap1 ((R_EAL f),x)) = {} & dom (ProjPMap1 (|.(R_EAL f).|,x)) = {} ) by A1, A2, Th25; :: thesis: verum