let G be non empty multMagma ; :: thesis: for g, g1, g2 being Element of G holds {g1,g2} * {g} = {(g1 * g),(g2 * g)}

let g, g1, g2 be Element of G; :: thesis: {g1,g2} * {g} = {(g1 * g),(g2 * g)}

thus {g1,g2} * {g} c= {(g1 * g),(g2 * g)} :: according to XBOOLE_0:def 10 :: thesis: {(g1 * g),(g2 * g)} c= {g1,g2} * {g}

A5: g2 in {g1,g2} by TARSKI:def 2;

assume x in {(g1 * g),(g2 * g)} ; :: thesis: x in {g1,g2} * {g}

then A6: ( x = g1 * g or x = g2 * g ) by TARSKI:def 2;

( g in {g} & g1 in {g1,g2} ) by TARSKI:def 1, TARSKI:def 2;

hence x in {g1,g2} * {g} by A6, A5; :: thesis: verum

let g, g1, g2 be Element of G; :: thesis: {g1,g2} * {g} = {(g1 * g),(g2 * g)}

thus {g1,g2} * {g} c= {(g1 * g),(g2 * g)} :: according to XBOOLE_0:def 10 :: thesis: {(g1 * g),(g2 * g)} c= {g1,g2} * {g}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(g1 * g),(g2 * g)} or x in {g1,g2} * {g} )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {g1,g2} * {g} or x in {(g1 * g),(g2 * g)} )

assume x in {g1,g2} * {g} ; :: thesis: x in {(g1 * g),(g2 * g)}

then consider h1, h2 being Element of G such that

A1: x = h1 * h2 and

A2: h1 in {g1,g2} and

A3: h2 in {g} ;

A4: ( h1 = g1 or h1 = g2 ) by A2, TARSKI:def 2;

h2 = g by A3, TARSKI:def 1;

hence x in {(g1 * g),(g2 * g)} by A1, A4, TARSKI:def 2; :: thesis: verum

end;assume x in {g1,g2} * {g} ; :: thesis: x in {(g1 * g),(g2 * g)}

then consider h1, h2 being Element of G such that

A1: x = h1 * h2 and

A2: h1 in {g1,g2} and

A3: h2 in {g} ;

A4: ( h1 = g1 or h1 = g2 ) by A2, TARSKI:def 2;

h2 = g by A3, TARSKI:def 1;

hence x in {(g1 * g),(g2 * g)} by A1, A4, TARSKI:def 2; :: thesis: verum

A5: g2 in {g1,g2} by TARSKI:def 2;

assume x in {(g1 * g),(g2 * g)} ; :: thesis: x in {g1,g2} * {g}

then A6: ( x = g1 * g or x = g2 * g ) by TARSKI:def 2;

( g in {g} & g1 in {g1,g2} ) by TARSKI:def 1, TARSKI:def 2;

hence x in {g1,g2} * {g} by A6, A5; :: thesis: verum