let n be Nat; :: thesis: for f being Element of REAL * holds dom ((Relax n) . f) = dom f
let f be Element of REAL * ; :: thesis: dom ((Relax n) . f) = dom f
thus dom ((Relax n) . f) = dom (Relax (f,n)) by Def15
.= dom f by Def14 ; :: thesis: verum