theorem Th36: :: GRAPHSP:36

for i, n being Nat
for f being Element of REAL * st ( i <= n or i > 3 * n ) & i in dom f holds
((Relax n) . f) . i = f . i