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:3
.= {((b ") * a)} * {b} by GROUP_2:18
.= {(a |^ b)} by GROUP_2:18 ;
( {a} |^ {b} c= (({b} ") * {a}) * {b} & {a} |^ {b} <> {} ) by Th32, Th33;
hence {a} |^ {b} = {(a |^ b)} by A1, ZFMISC_1:33; :: thesis: verum