let G be addGroup; :: thesis:
thus ( G is Abelian addGroup implies for A, B being Subset of G st B <> {} holds
A * B = A ) :: thesis:

assume A1: G is Abelian addGroup ; :: thesis:
let A, B be Subset of G; :: thesis:
set y = the Element of B;
assume A2: B <> {} ; :: thesis:
then reconsider y = the Element of B as Element of G by TARSKI:def 3;
thus A * B c= A :: according to XBOOLE_0:def 10 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in A * B ; :: thesis:
then ex a, b being Element of G st
( x = a * b & a in A & b in B ) ;
hence x in A by A1, Th29; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A3: x in A ; :: thesis:
then reconsider a = x as Element of G ;
a * y = x by A1, Th29;
hence x in A * B by A2, A3; :: thesis:

end;

let a, b be Element of G; :: thesis:
{a} = {a} * {b} by A4
.= {(a * b)} by ThB37 ;
hence a = a * b by ZFMISC_1:3; :: thesis:

end;