set G = HomeoGroup T;
set o = the multF of (HomeoGroup T);
thus HomeoGroup T is Group-like :: thesis: HomeoGroup T is associative

proof

reconsider e = id T as Element of (HomeoGroup T) by Def5;
take e ; :: according to GROUP_1:def 2 :: thesis: for b₁ being Element of the carrier of (HomeoGroup T) holds
( b₁ * e = b₁ & e * b₁ = b₁ & ex b₂ being Element of the carrier of (HomeoGroup T) st
( b₁ * b₂ = e & b₂ * b₁ = e ) )
let h be Element of (HomeoGroup T); :: thesis: ( h * e = h & e * h = h & ex b₁ being Element of the carrier of (HomeoGroup T) st
( h * b₁ = e & b₁ * h = e ) )
reconsider h1 = h, e1 = e as Homeomorphism of T by Def5;
thus h * e = e1 * h1 by Def5
.= h by FUNCT_2:17 ; :: thesis: ( e * h = h & ex b₁ being Element of the carrier of (HomeoGroup T) st
( h * b₁ = e & b₁ * h = e ) )
thus e * h = h1 * e1 by Def5
.= h by FUNCT_2:17 ; :: thesis: ex b₁ being Element of the carrier of (HomeoGroup T) st
( h * b₁ = e & b₁ * h = e )
reconsider h1 = h as Homeomorphism of T by Def5;
A1: dom h1 = [#] T by TOPS_2:def 5;
h1 /" is Homeomorphism of T by Th29;
then reconsider g = h1 /" as Element of (HomeoGroup T) by Def5;
reconsider g1 = g as Homeomorphism of T by Def5;
take g ; :: thesis: ( h * g = e & g * h = e )
A2: rng h1 = [#] T by TOPS_2:def 5;
thus h * g = g1 * h1 by Def5
.= e by A1, A2, TOPS_2:52 ; :: thesis: g * h = e
thus g * h = h1 * g1 by Def5
.= e by A2, TOPS_2:52 ; :: thesis: verum

end;

let x, y, z be Element of (HomeoGroup T); :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)
reconsider f = x, g = y as Homeomorphism of T by Def5;
reconsider p = g * f, r = z as Homeomorphism of T by Def5, Th30;
reconsider a = r * g as Homeomorphism of T by Th30;
thus (x * y) * z = the multF of (HomeoGroup T) . ((g * f),z) by Def5
.= r * p by Def5
.= (r * g) * f by RELAT_1:36
.= the multF of (HomeoGroup T) . (f,a) by Def5
.= x * (y * z) by Def5 ; :: thesis: verum