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