defpred S₁[ 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 S₁[x,y,z]

proof

let x, y be Element of ISOM (RLMSpace n); :: thesis: ex z being Element of ISOM (RLMSpace n) st S₁[x,y,z]
consider x1 being Function of (RLMSpace n),(RLMSpace n) such that
A2: x1 = x and
A3: x1 is isometric by Def4;
consider y1 being Function of (RLMSpace n),(RLMSpace n) such that
A4: y1 = y and
A5: y1 is isometric by Def4;
x1 * y1 is isometric by A3, A5, Th4;
then reconsider z = x1 * y1 as Element of ISOM (RLMSpace n) by Def4;
take z ; :: thesis: S₁[x,y,z]
take x1 ; :: thesis: ex g being Function st
( x1 = x & g = y & z = x1 * g )
take y1 ; :: thesis: ( x1 = x & y1 = y & z = x1 * y1 )
thus ( x1 = x & y1 = y & z = x1 * y1 ) by A2, A4; :: thesis: verum

end;

consider o being BinOp of (ISOM (RLMSpace n)) such that
A6: for a, b being Element of ISOM (RLMSpace n) holds S₁[a,b,o . a,b] from BINOP_1:sch 3(A1);
take G = multMagma(# (ISOM (RLMSpace n)),o #); :: thesis: ( 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

proof

let f, g be Function; :: thesis: ( f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) implies the multF of G . f,g = f * g )
assume ( f in ISOM (RLMSpace n) & g in ISOM (RLMSpace n) ) ; :: thesis: the multF of G . f,g = f * g
then ex f1, g1 being Function st
( f1 = f & g1 = g & o . f,g = f1 * g1 ) by A6;
hence the multF of G . f,g = f * g ; :: thesis: verum

end;

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