let G be Group; :: thesis: for A being Subgroup of G
for a being Element of G holds
( (a * A) * A = a * A & a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a )
let A be Subgroup of G; :: thesis: for a being Element of G holds
( (a * A) * A = a * A & a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a )
let a be Element of G; :: thesis: ( (a * A) * A = a * A & a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a )
thus (a * A) * A = a * (A * A) by GROUP_4:45
.= a * A by GROUP_2:76 ; :: thesis: ( a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a )
hence a * (A * A) = a * A by GROUP_4:45; :: thesis: ( (A * A) * a = A * a & A * (A * a) = A * a )
thus (A * A) * a = A * a by GROUP_2:76; :: thesis: A * (A * a) = A * a
hence A * (A * a) = A * a by GROUP_4:46; :: thesis: verum