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
reconsider f1 = f as Function of (RLMSpace n),(RLMSpace n) by A7, Def4;
reconsider g1 = g as Function of (RLMSpace n),(RLMSpace n) by A7, Def4;
thus the multF of G1 . f,g = f1 * g1 by A7, A8
.= the multF of G2 . f,g by A7, A10 ; :: thesis: verum

end;

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