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

let h be Element of (IsomGroup n); :: thesis:
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:
thus e * h = (id the carrier of (RLMSpace n)) * h1 by A1, A2, Def9
.= h by FUNCT_2:17 ; :: thesis:

end;