let G be Group; :: thesis: for a being Element of G
for H being Subgroup of G holds the carrier of (H |^ a) = ((a " ) * H) * a
let a be Element of G; :: thesis: for H being Subgroup of G holds the carrier of (H |^ a) = ((a " ) * H) * a
let H be Subgroup of G; :: thesis: the carrier of (H |^ a) = ((a " ) * H) * a
thus the carrier of (H |^ a) = (carr H) |^ a by Def6
.= ((a " ) * H) * a by Th59 ; :: thesis: verum