for n, m being Nat holds dom ((R_EAL f) . n) = dom ((R_EAL f) . m) by MESFUNC8:def 2;
hence R_EAL f is with_the_same_dom by MESFUNC8:def 2; :: thesis: verum