let G be non empty multMagma ; :: thesis: for g, g1, g2 being Element of G holds {g} * {g1,g2} = {(g * g1),(g * g2)}
let g, g1, g2 be Element of G; :: thesis: {g} * {g1,g2} = {(g * g1),(g * g2)}
thus {g} * {g1,g2} c= {(g * g1),(g * g2)} :: according to XBOOLE_0:def 10 :: thesis: {(g * g1),(g * g2)} c= {g} * {g1,g2}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {g} * {g1,g2} or x in {(g * g1),(g * g2)} )
assume x in {g} * {g1,g2} ; :: thesis: x in {(g * g1),(g * g2)}
then consider h1, h2 being Element of G such that
A1: x = h1 * h2 and
A2: ( h1 in {g} & h2 in {g1,g2} ) ;
( h1 = g & ( h2 = g1 or h2 = g2 ) ) by A2, TARSKI:def 1, TARSKI:def 2;
hence x in {(g * g1),(g * g2)} by A1, TARSKI:def 2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(g * g1),(g * g2)} or x in {g} * {g1,g2} )
assume x in {(g * g1),(g * g2)} ; :: thesis: x in {g} * {g1,g2}
then ( ( x = g * g1 or x = g * g2 ) & g in {g} & g1 in {g1,g2} & g2 in {g1,g2} ) by TARSKI:def 1, TARSKI:def 2;
hence x in {g} * {g1,g2} ; :: thesis: verum