let G be addGroup; :: thesis: for a, b, c being Element of G holds {a,b} * {c} = {(a * c),(b * c)}
let a, b, c be Element of G; :: thesis: {a,b} * {c} = {(a * c),(b * c)}
thus {a,b} * {c} c= {(a * c),(b * c)} :: according to XBOOLE_0:def 10 :: thesis: {(a * c),(b * c)} c= {a,b} * {c}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {a,b} * {c} or x in {(a * c),(b * c)} )
assume x in {a,b} * {c} ; :: thesis: x in {(a * c),(b * c)}
then consider g, h being Element of G such that
A1: x = g * h and
A2: g in {a,b} and
A3: h in {c} ;
A4: ( g = b or g = a ) by A2, TARSKI:def 2;
h = c by A3, TARSKI:def 1;
hence x in {(a * c),(b * c)} by A1, A4, TARSKI:def 2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(a * c),(b * c)} or x in {a,b} * {c} )
A5: c in {c} by TARSKI:def 1;
assume x in {(a * c),(b * c)} ; :: thesis: x in {a,b} * {c}
then A6: ( x = a * c or x = b * c ) by TARSKI:def 2;
( a in {a,b} & b in {a,b} ) by TARSKI:def 2;
hence x in {a,b} * {c} by A6, A5; :: thesis: verum