defpred S1[ set , set , set ] means ex f, g being Function st
( f = $1 & g = $2 & $3 = f * g );
A1:
for x, y being Element of ISOM (RLMSpace n) ex z being Element of ISOM (RLMSpace n) st S1[x,y,z]
consider o being BinOp of (ISOM (RLMSpace n)) such that
A2:
for a, b being Element of ISOM (RLMSpace n) holds S1[a,b,o . (a,b)]
from BINOP_1:sch 3(A1);
take G = multMagma(# (ISOM (RLMSpace n)),o #); ( the carrier of G = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds
the multF of G . (f,g) = f * g ) )
for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds
the multF of G . (f,g) = f * g
hence
( the carrier of G = ISOM (RLMSpace n) & ( for f, g being Function st f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) holds
the multF of G . (f,g) = f * g ) )
; verum