let G be Group; :: thesis: for a, b being Element of G holds {a} |^ {b} = {(a |^ b)}
let a, b be Element of G; :: thesis: {a} |^ {b} = {(a |^ b)}
A1: (({b} " ) * {a}) * {b} = ({(b " )} * {a}) * {b} by GROUP_2:6
.= {((b " ) * a)} * {b} by GROUP_2:22
.= {(a |^ b)} by GROUP_2:22 ;
( {a} |^ {b} c= (({b} " ) * {a}) * {b} & {a} |^ {b} <> {} ) by Th39, Th40;
hence {a} |^ {b} = {(a |^ b)} by A1, ZFMISC_1:39; :: thesis: verum