( G ./. N is associative & G ./. N is Group-like )

proof

thus for f, g, h being Element of (G ./. N) holds f * (g * h) = (f * g) * h :: according to GROUP_1:def 4 :: 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 & f = N * a ) by Th15;
consider c being Element of G such that
A2: ( h = c * N & h = N * c ) by Th15;
thus f * (g * h) = (@ f) * (@ (g * h)) by Def4
.= (a * N) * ((@ g) * (@ h)) by A1, Def4
.= ((@ f) * (@ g)) * (c * N) by A1, A2, GROUP_2:14
.= (@ (f * g)) * (@ h) by A2, Def4
.= (f * g) * h by Def4 ; :: thesis: verum

end;

reconsider e = carr N as Element of (G ./. N) by GROUP_2:165;
take e ; :: according to GROUP_1:def 3 :: 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 & h = N * a ) by Th15;
thus h * e = (a * N) * N by A3, Def4
.= a * (N * N) by GROUP_4:60
.= h by A3, GROUP_2:91 ; :: 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 A3, Def4
.= (N * N) * a by GROUP_4:61
.= h by A3, GROUP_2:91 ; :: 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 A3, Def4
.= ((N * a) * (a " )) * N by GROUP_3:10
.= (N * (a * (a " ))) * N by GROUP_2:129
.= (N * (1_ G)) * N by GROUP_1:def 6
.= (carr N) * (carr N) by GROUP_2:132
.= e by GROUP_2:91 ; :: thesis: g * h = e
thus g * h = (@ g) * (@ h) by Def4
.= (((a " ) * N) * a) * N by A3, GROUP_3:10
.= ((a " ) * (N * a)) * N by GROUP_2:128
.= ((a " ) * (a * N)) * N by GROUP_3:140
.= (((a " ) * a) * N) * N by GROUP_2:127
.= ((1_ G) * N) * N by GROUP_1:def 6
.= (1_ G) * (N * N) by GROUP_4:60
.= (1_ G) * (carr N) by GROUP_2:91
.= e by GROUP_2:43 ; :: thesis: verum

end;

hence ( G ./. N is associative & G ./. N is Group-like ) ; :: thesis: verum