let G be addGroup; :: thesis: for g being Element of G
for A being Subset of G holds A * g = ((- g) + A) + g
let g be Element of G; :: thesis: for A being Subset of G holds A * g = ((- g) + A) + g
let A be Subset of G; :: thesis: A * g = ((- g) + A) + g
A * g c= ((- {g}) + A) + {g} by ThB33;
hence A * g c= ((- g) + A) + g by ThB3; :: according to XBOOLE_0:def 10 :: thesis: ((- g) + A) + g c= A * g
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((- g) + A) + g or x in A * g )
assume x in ((- g) + A) + g ; :: thesis: x in A * g
then consider a being Element of G such that
A1: x = a + g and
A2: a in (- g) + A by Th28;
consider b being Element of G such that
A3: a = (- g) + b and
A4: b in A by A2, Th27;
x = b * g by A1, A3;
hence x in A * g by A4, Th41; :: thesis: verum