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

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 ; :: thesis: G1 = G2

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

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 ; :: thesis: G1 = G2

now :: thesis: for f, g being Element of G1 holds the multF of G1 . (f,g) = the multF of G2 . (f,g)

hence
G1 = G2
by A3, A5, BINOP_1:2; :: thesis: verumlet 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 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 ; :: thesis: verum

end;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 ; :: thesis: verum