for n being Nat
for f being Element of REAL * holds dom ((Relax n) . f) = dom f