theorem Th35: :: GRAPHSP:35

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