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]
proof
let x, y be Element of ISOM (RLMSpace n); :: thesis: ex z being Element of ISOM (RLMSpace n) st S1[x,y,z]
reconsider x1 = x as onto isometric Function of (RLMSpace n),(RLMSpace n) by Def4;
reconsider y1 = y as onto isometric Function of (RLMSpace n),(RLMSpace n) by Def4;
reconsider z = x1 * y1 as Element of ISOM (RLMSpace n) by Def4;
take z ; :: thesis: S1[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 ) ; :: thesis: verum
end;
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 #); :: 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 A2;
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