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

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

set A = {g,h} * {g1,g2};

set B = {(g * g1),(g * g2),(h * g1),(h * g2)};

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

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

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

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

( g in {g,h} & h in {g,h} ) by TARSKI:def 2;

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

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

set A = {g,h} * {g1,g2};

set B = {(g * g1),(g * g2),(h * g1),(h * g2)};

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

proof

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

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

then consider h1, h2 being Element of G such that

A1: x = h1 * h2 and

A2: h1 in {g,h} and

A3: h2 in {g1,g2} ;

A4: ( h2 = g1 or h2 = g2 ) by A3, TARSKI:def 2;

( h1 = g or h1 = h ) by A2, TARSKI:def 2;

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

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

then consider h1, h2 being Element of G such that

A1: x = h1 * h2 and

A2: h1 in {g,h} and

A3: h2 in {g1,g2} ;

A4: ( h2 = g1 or h2 = g2 ) by A3, TARSKI:def 2;

( h1 = g or h1 = h ) by A2, TARSKI:def 2;

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

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

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

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

( g in {g,h} & h in {g,h} ) by TARSKI:def 2;

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