:: deftheorem Def9 defines IsomGroup VECTMETR:def 9 :
for n being Element of NAT
for b₂ being strict multMagma holds
( b₂ = IsomGroup n iff ( the carrier of b₂ = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds
the multF of b₂ . (f,g) = f * g ) ) );