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;

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 )

hence
1_ (IsomGroup n) = id (RLMSpace n)
by GROUP_1:4; :: thesis: verum( 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;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