set V = RLMSpace n;
let G1, G2 be strict multMagma ; :: thesis: ( the carrier of G1 = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds
the multF of G1 . f,g = f * g ) & the carrier of G2 = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds
the multF of G2 . f,g = f * g ) implies G1 = G2 )
assume that
A7: the carrier of G1 = ISOM (RLMSpace n) and
A8: for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds
the multF of G1 . f,g = f * g and
A9: the carrier of G2 = ISOM (RLMSpace n) and
A10: for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds
the multF of G2 . f,g = f * g ; :: thesis: G1 = G2

now

let f, g be Element of G1; :: thesis: the multF of G1 . f,g = the multF of G2 . f,g
consider f1 being Function of (RLMSpace n),(RLMSpace n) such that
A11: f1 = f and
f1 is isometric by A7, Def4;
consider g1 being Function of (RLMSpace n),(RLMSpace n) such that
A12: g1 = g and
g1 is isometric by A7, Def4;
thus the multF of G1 . f,g = f1 * g1 by A7, A8, A11, A12
.= the multF of G2 . f,g by A7, A10, A11, A12 ; :: thesis: verum

end;

hence G1 = G2 by A7, A9, BINOP_1:2; :: thesis: verum