thus for f, g, h being Element of (G ./. N) holds f * (g * h) = (f * g) * h :: according to GROUP_1:def 3 :: thesis: G ./. N is Group-like

proof

let f, g, h be Element of (G ./. N); :: thesis: f * (g * h) = (f * g) * h
consider a being Element of G such that
A1: f = a * N and
f = N * a by Th13;
consider c being Element of G such that
A2: h = c * N and
h = N * c by Th13;
thus f * (g * h) = (@ f) * (@ (g * h)) by Def3
.= (a * N) * ((@ g) * (@ h)) by A1, Def3
.= ((@ f) * (@ g)) * (c * N) by A1, A2, GROUP_2:10
.= (@ (f * g)) * (@ h) by A2, Def3
.= (f * g) * h by Def3 ; :: thesis: verum

end;

reconsider e = carr N as Element of (G ./. N) by GROUP_2:135;
take e ; :: according to GROUP_1:def 2 :: thesis: for b₁ being Element of the carrier of (G ./. N) holds
( b₁ * e = b₁ & e * b₁ = b₁ & ex b₂ being Element of the carrier of (G ./. N) st
( b₁ * b₂ = e & b₂ * b₁ = e ) )
let h be Element of (G ./. N); :: thesis: ( h * e = h & e * h = h & ex b₁ being Element of the carrier of (G ./. N) st
( h * b₁ = e & b₁ * h = e ) )
consider a being Element of G such that
A3: h = a * N and
A4: h = N * a by Th13;
thus h * e = (a * N) * N by A3, Def3
.= a * (N * N) by GROUP_4:45
.= h by A3, GROUP_2:76 ; :: thesis: ( e * h = h & ex b₁ being Element of the carrier of (G ./. N) st
( h * b₁ = e & b₁ * h = e ) )
thus e * h = N * (N * a) by A4, Def3
.= (N * N) * a by GROUP_4:46
.= h by A4, GROUP_2:76 ; :: thesis: ex b₁ being Element of the carrier of (G ./. N) st
( h * b₁ = e & b₁ * h = e )
reconsider g = (a ") * N as Element of (G ./. N) by GROUP_2:def 15;
take g ; :: thesis: ( h * g = e & g * h = e )
thus h * g = (N * a) * ((a ") * N) by A4, Def3
.= ((N * a) * (a ")) * N by GROUP_3:9
.= (N * (a * (a "))) * N by GROUP_2:107
.= (N * (1_ G)) * N by GROUP_1:def 5
.= (carr N) * (carr N) by GROUP_2:109
.= e by GROUP_2:76 ; :: thesis: g * h = e
thus g * h = (@ g) * (@ h) by Def3
.= (((a ") * N) * a) * N by A3, GROUP_3:9
.= ((a ") * (N * a)) * N by GROUP_2:106
.= ((a ") * (a * N)) * N by GROUP_3:117
.= (((a ") * a) * N) * N by GROUP_2:105
.= ((1_ G) * N) * N by GROUP_1:def 5
.= (1_ G) * (N * N) by GROUP_4:45
.= (1_ G) * (carr N) by GROUP_2:76
.= e by GROUP_2:37 ; :: thesis: verum