let X, Y be non empty set ; :: thesis: for A being Subset of X
for B being Subset of Y
for y being Element of Y
for f being PartFunc of [:X,Y:],REAL st dom f = [:A,B:] holds
( ( y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = A & dom (ProjPMap2 (|.(R_EAL f).|,y)) = A ) ) & ( not y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = {} & dom (ProjPMap2 (|.(R_EAL f).|,y)) = {} ) ) )
let A be Subset of X; :: thesis: for B being Subset of Y
for y being Element of Y
for f being PartFunc of [:X,Y:],REAL st dom f = [:A,B:] holds
( ( y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = A & dom (ProjPMap2 (|.(R_EAL f).|,y)) = A ) ) & ( not y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = {} & dom (ProjPMap2 (|.(R_EAL f).|,y)) = {} ) ) )
let B be Subset of Y; :: thesis: for y being Element of Y
for f being PartFunc of [:X,Y:],REAL st dom f = [:A,B:] holds
( ( y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = A & dom (ProjPMap2 (|.(R_EAL f).|,y)) = A ) ) & ( not y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = {} & dom (ProjPMap2 (|.(R_EAL f).|,y)) = {} ) ) )
let y be Element of Y; :: thesis: for f being PartFunc of [:X,Y:],REAL st dom f = [:A,B:] holds
( ( y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = A & dom (ProjPMap2 (|.(R_EAL f).|,y)) = A ) ) & ( not y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = {} & dom (ProjPMap2 (|.(R_EAL f).|,y)) = {} ) ) )
let f be PartFunc of [:X,Y:],REAL; :: thesis: ( dom f = [:A,B:] implies ( ( y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = A & dom (ProjPMap2 (|.(R_EAL f).|,y)) = A ) ) & ( not y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = {} & dom (ProjPMap2 (|.(R_EAL f).|,y)) = {} ) ) ) )
assume dom f = [:A,B:] ; :: thesis: ( ( y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = A & dom (ProjPMap2 (|.(R_EAL f).|,y)) = A ) ) & ( not y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = {} & dom (ProjPMap2 (|.(R_EAL f).|,y)) = {} ) ) )
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 ( y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = A & dom (ProjPMap2 (|.(R_EAL f).|,y)) = A ) ) by A1, Th26; :: thesis: ( not y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = {} & dom (ProjPMap2 (|.(R_EAL f).|,y)) = {} ) )
assume not y in B ; :: thesis: ( dom (ProjPMap2 ((R_EAL f),y)) = {} & dom (ProjPMap2 (|.(R_EAL f).|,y)) = {} )
hence ( dom (ProjPMap2 ((R_EAL f),y)) = {} & dom (ProjPMap2 (|.(R_EAL f).|,y)) = {} ) by A1, A2, Th26; :: thesis: verum