theorem Th37: :: GRAPHSP:37

for i, n being Nat
for f being Element of REAL * holds dom (((repeat ((Relax n) * (findmin n))) . i) . f) = dom (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f)