let H be Subgroup of G; :: thesis: H is associative

let x, y, z be Element of H; :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)

( y * z in the carrier of H & the carrier of H c= the carrier of G ) by Def5;

then reconsider a = x, b = y, c = z, ab = x * y, bc = y * z as Element of G ;

thus (x * y) * z = ab * c by Th43

.= (a * b) * c by Th43

.= a * (b * c) by GROUP_1:def 3

.= a * bc by Th43

.= x * (y * z) by Th43 ; :: thesis: verum

let x, y, z be Element of H; :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)

( y * z in the carrier of H & the carrier of H c= the carrier of G ) by Def5;

then reconsider a = x, b = y, c = z, ab = x * y, bc = y * z as Element of G ;

thus (x * y) * z = ab * c by Th43

.= (a * b) * c by Th43

.= a * (b * c) by GROUP_1:def 3

.= a * bc by Th43

.= x * (y * z) by Th43 ; :: thesis: verum