let n be Element of NAT ; :: thesis: for f being isometric Function of (RLMSpace n),(RLMSpace n) holds rng f = REAL n
let f be isometric Function of (RLMSpace n),(RLMSpace n); :: thesis: rng f = REAL n
thus rng f = the carrier of (RLMSpace n) by Def3
.= REAL n by Def8 ; :: thesis: verum