let n be Element of NAT ; :: thesis: 1_ (IsomGroup n) = id (RLMSpace n)
id (RLMSpace n) is isometric by Th5;
then A1: id (RLMSpace n) in ISOM (RLMSpace n) by Def4;
then reconsider e = id (RLMSpace n) as Element of (IsomGroup n) by Def9;

now

let h be Element of (IsomGroup n); :: thesis: ( h * e = h & e * h = h )
h in the carrier of (IsomGroup n) ;
then A2: h in ISOM (RLMSpace n) by Def9;
then consider h1 being Function of (RLMSpace n),(RLMSpace n) such that
A3: h1 = h and
h1 is isometric by Def4;
thus h * e = h1 * (id the carrier of (RLMSpace n)) by A1, A2, A3, Def9
.= h by A3, FUNCT_2:23 ; :: thesis: e * h = h
thus e * h = (id the carrier of (RLMSpace n)) * h1 by A1, A2, A3, Def9
.= h by A3, FUNCT_2:23 ; :: thesis: verum

end;

hence 1_ (IsomGroup n) = id (RLMSpace n) by GROUP_1:10; :: thesis: verum