let G be addGroup; :: 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 ThB3
.= {((- b) + a)} + {b} by Th18
.= {(a * b)} by Th18 ;
( {a} * {b} c= ((- {b}) + {a}) + {b} & {a} * {b} <> {} ) by ThB32, ThB33;
hence {a} * {b} = {(a * b)} by A1, ZFMISC_1:33; :: thesis: verum