set V = RLMSpace n;
let G1, G2 be strict multMagma ; ( 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
A3:
the carrier of G1 = ISOM (RLMSpace n)
and
A4:
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
A5:
the carrier of G2 = ISOM (RLMSpace n)
and
A6:
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
; G1 = G2
now for f, g being Element of G1 holds the multF of G1 . (f,g) = the multF of G2 . (f,g)let f,
g be
Element of
G1;
the multF of G1 . (f,g) = the multF of G2 . (f,g)reconsider f1 =
f as
Function of
(RLMSpace n),
(RLMSpace n) by A3, Def4;
reconsider g1 =
g as
Function of
(RLMSpace n),
(RLMSpace n) by A3, Def4;
thus the
multF of
G1 . (
f,
g) =
f1 * g1
by A3, A4
.=
the
multF of
G2 . (
f,
g)
by A3, A6
;
verum end;
hence
G1 = G2
by A3, A5, BINOP_1:2; verum