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

now :: thesis: for h being Element of (IsomGroup n) holds
( h * e = h & e * h = h )

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 reconsider h1 = h as Function of (RLMSpace n),(RLMSpace n) by Def4;
thus h * e = h1 * (id the carrier of (RLMSpace n)) by A1, A2, Def9
.= h by FUNCT_2:17 ; :: thesis: e * h = h
thus e * h = (id the carrier of (RLMSpace n)) * h1 by A1, A2, Def9
.= h by FUNCT_2:17 ; :: thesis: verum

end;

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