now :: thesis: for x, y, z being Element of () holds (x * y) * z = x * (y * z)
let x, y, z be Element of (); :: thesis: (x * y) * z = x * (y * z)
x in the carrier of () ;
then A1: x in ISOM () by Def9;
then reconsider x1 = x as onto isometric Function of (),() by Def4;
y in the carrier of () ;
then A2: y in ISOM () by Def9;
then reconsider y1 = y as onto isometric Function of (),() by Def4;
A3: x1 * y1 in ISOM () by Def4;
z in the carrier of () ;
then A4: z in ISOM () by Def9;
then reconsider z1 = z as onto isometric Function of (),() by Def4;
A5: y1 * z1 in ISOM () by Def4;
thus (x * y) * z = the multF of () . ((x1 * y1),z) by A1, A2, Def9
.= (x1 * y1) * z1 by A4, A3, Def9
.= x1 * (y1 * z1) by RELAT_1:36
.= the multF of () . (x,(y1 * z1)) by A1, A5, Def9
.= x * (y * z) by A2, A4, Def9 ; :: thesis: verum
end;
hence IsomGroup n is associative by GROUP_1:def 3; :: thesis:
ex e being Element of () st
for h being Element of () holds
( h * e = h & e * h = h & ex g being Element of () st
( h * g = e & g * h = e ) )
proof
A6: id () in ISOM () by Def4;
then reconsider e = id () as Element of () by Def9;
take e ; :: thesis: for h being Element of () holds
( h * e = h & e * h = h & ex g being Element of () st
( h * g = e & g * h = e ) )

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

h in the carrier of () ;
then A7: h in ISOM () by Def9;
then reconsider h1 = h as onto isometric Function of (),() by Def4;
thus h * e = h1 * (id the carrier of ()) by A6, A7, Def9
.= h by FUNCT_2:17 ; :: thesis: ( e * h = h & ex g being Element of () st
( h * g = e & g * h = e ) )

thus e * h = (id the carrier of ()) * h1 by A6, A7, Def9
.= h by FUNCT_2:17 ; :: thesis: ex g being Element of () st
( h * g = e & g * h = e )

A8: rng h1 = [#] () by FUNCT_2:def 3;
A9: h1 " in ISOM () by Def4;
then reconsider g = h1 " as Element of () by Def9;
take g ; :: thesis: ( h * g = e & g * h = e )
thus h * g = h1 * (h1 ") by A7, A9, Def9
.= e by ; :: thesis: g * h = e
thus g * h = (h1 ") * h1 by A7, A9, Def9
.= id (dom h1) by
.= e by FUNCT_2:def 1 ; :: thesis: verum
end;
hence IsomGroup n is Group-like by GROUP_1:def 2; :: thesis: verum