theorem Th7: :: VECTMETR:10

for n being Element of NAT holds 1_ (IsomGroup n) = id (RLMSpace n)