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

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