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