defpred S_{1}[ 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_{1}[x,y,z]

A2: for a, b being Element of ISOM (RLMSpace n) holds S_{1}[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

the multF of G . (f,g) = f * g ) ) ; :: thesis: verum

( 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

proof

consider o being BinOp of (ISOM (RLMSpace n)) such that
let x, y be Element of ISOM (RLMSpace n); :: thesis: ex z being Element of ISOM (RLMSpace n) st S_{1}[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: S_{1}[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;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: S

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

A2: for a, b being Element of ISOM (RLMSpace n) holds S

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

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
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;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

the multF of G . (f,g) = f * g ) ) ; :: thesis: verum