let i, n be Nat; :: thesis: for f being Element of REAL * st ( i <= n or i > 3 * n ) & i in dom f holds
((Relax n) . f) . i = f . i
let f be Element of REAL * ; :: thesis: ( ( i <= n or i > 3 * n ) & i in dom f implies ((Relax n) . f) . i = f . i )
assume A1: ( ( i <= n or i > 3 * n ) & i in dom f ) ; :: thesis: ((Relax n) . f) . i = f . i
thus ((Relax n) . f) . i = (Relax (f,n)) . i by Def15
.= f . i by A1, Def14 ; :: thesis: verum