now :: thesis: for x, y, z being Element of (IsomGroup n) holds (x * y) * z = x * (y * z)

hence
IsomGroup n is associative
by GROUP_1:def 3; :: thesis: IsomGroup n is Group-like let x, y, z be Element of (IsomGroup n); :: thesis: (x * y) * z = x * (y * z)

x in the carrier of (IsomGroup n) ;

then A1: x in ISOM (RLMSpace n) by Def9;

then reconsider x1 = x as onto isometric Function of (RLMSpace n),(RLMSpace n) by Def4;

y in the carrier of (IsomGroup n) ;

then A2: y in ISOM (RLMSpace n) by Def9;

then reconsider y1 = y as onto isometric Function of (RLMSpace n),(RLMSpace n) by Def4;

A3: x1 * y1 in ISOM (RLMSpace n) by Def4;

z in the carrier of (IsomGroup n) ;

then A4: z in ISOM (RLMSpace n) by Def9;

then reconsider z1 = z as onto isometric Function of (RLMSpace n),(RLMSpace n) by Def4;

A5: y1 * z1 in ISOM (RLMSpace n) by Def4;

thus (x * y) * z = the multF of (IsomGroup n) . ((x1 * y1),z) by A1, A2, Def9

.= (x1 * y1) * z1 by A4, A3, Def9

.= x1 * (y1 * z1) by RELAT_1:36

.= the multF of (IsomGroup n) . (x,(y1 * z1)) by A1, A5, Def9

.= x * (y * z) by A2, A4, Def9 ; :: thesis: verum

end;x in the carrier of (IsomGroup n) ;

then A1: x in ISOM (RLMSpace n) by Def9;

then reconsider x1 = x as onto isometric Function of (RLMSpace n),(RLMSpace n) by Def4;

y in the carrier of (IsomGroup n) ;

then A2: y in ISOM (RLMSpace n) by Def9;

then reconsider y1 = y as onto isometric Function of (RLMSpace n),(RLMSpace n) by Def4;

A3: x1 * y1 in ISOM (RLMSpace n) by Def4;

z in the carrier of (IsomGroup n) ;

then A4: z in ISOM (RLMSpace n) by Def9;

then reconsider z1 = z as onto isometric Function of (RLMSpace n),(RLMSpace n) by Def4;

A5: y1 * z1 in ISOM (RLMSpace n) by Def4;

thus (x * y) * z = the multF of (IsomGroup n) . ((x1 * y1),z) by A1, A2, Def9

.= (x1 * y1) * z1 by A4, A3, Def9

.= x1 * (y1 * z1) by RELAT_1:36

.= the multF of (IsomGroup n) . (x,(y1 * z1)) by A1, A5, Def9

.= x * (y * z) by A2, A4, Def9 ; :: thesis: verum

ex e being Element of (IsomGroup n) st

for h being Element of (IsomGroup n) holds

( h * e = h & e * h = h & ex g being Element of (IsomGroup n) st

( h * g = e & g * h = e ) )

proof

hence
IsomGroup n is Group-like
by GROUP_1:def 2; :: thesis: verum
A6:
id (RLMSpace n) in ISOM (RLMSpace n)
by Def4;

then reconsider e = id (RLMSpace n) as Element of (IsomGroup n) by Def9;

take e ; :: thesis: for h being Element of (IsomGroup n) holds

( h * e = h & e * h = h & ex g being Element of (IsomGroup n) st

( h * g = e & g * h = e ) )

let h be Element of (IsomGroup n); :: thesis: ( h * e = h & e * h = h & ex g being Element of (IsomGroup n) st

( h * g = e & g * h = e ) )

h in the carrier of (IsomGroup n) ;

then A7: h in ISOM (RLMSpace n) by Def9;

then reconsider h1 = h as onto isometric Function of (RLMSpace n),(RLMSpace n) by Def4;

thus h * e = h1 * (id the carrier of (RLMSpace n)) by A6, A7, Def9

.= h by FUNCT_2:17 ; :: thesis: ( e * h = h & ex g being Element of (IsomGroup n) st

( h * g = e & g * h = e ) )

thus e * h = (id the carrier of (RLMSpace n)) * h1 by A6, A7, Def9

.= h by FUNCT_2:17 ; :: thesis: ex g being Element of (IsomGroup n) st

( h * g = e & g * h = e )

A8: rng h1 = [#] (RLMSpace n) by FUNCT_2:def 3;

A9: h1 " in ISOM (RLMSpace n) by Def4;

then reconsider g = h1 " as Element of (IsomGroup n) by Def9;

take g ; :: thesis: ( h * g = e & g * h = e )

thus h * g = h1 * (h1 ") by A7, A9, Def9

.= e by A8, TOPS_2:52 ; :: thesis: g * h = e

thus g * h = (h1 ") * h1 by A7, A9, Def9

.= id (dom h1) by A8, TOPS_2:52

.= e by FUNCT_2:def 1 ; :: thesis: verum

end;then reconsider e = id (RLMSpace n) as Element of (IsomGroup n) by Def9;

take e ; :: thesis: for h being Element of (IsomGroup n) holds

( h * e = h & e * h = h & ex g being Element of (IsomGroup n) st

( h * g = e & g * h = e ) )

let h be Element of (IsomGroup n); :: thesis: ( h * e = h & e * h = h & ex g being Element of (IsomGroup n) st

( h * g = e & g * h = e ) )

h in the carrier of (IsomGroup n) ;

then A7: h in ISOM (RLMSpace n) by Def9;

then reconsider h1 = h as onto isometric Function of (RLMSpace n),(RLMSpace n) by Def4;

thus h * e = h1 * (id the carrier of (RLMSpace n)) by A6, A7, Def9

.= h by FUNCT_2:17 ; :: thesis: ( e * h = h & ex g being Element of (IsomGroup n) st

( h * g = e & g * h = e ) )

thus e * h = (id the carrier of (RLMSpace n)) * h1 by A6, A7, Def9

.= h by FUNCT_2:17 ; :: thesis: ex g being Element of (IsomGroup n) st

( h * g = e & g * h = e )

A8: rng h1 = [#] (RLMSpace n) by FUNCT_2:def 3;

A9: h1 " in ISOM (RLMSpace n) by Def4;

then reconsider g = h1 " as Element of (IsomGroup n) by Def9;

take g ; :: thesis: ( h * g = e & g * h = e )

thus h * g = h1 * (h1 ") by A7, A9, Def9

.= e by A8, TOPS_2:52 ; :: thesis: g * h = e

thus g * h = (h1 ") * h1 by A7, A9, Def9

.= id (dom h1) by A8, TOPS_2:52

.= e by FUNCT_2:def 1 ; :: thesis: verum