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

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

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

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

then A3: x = g * h by TARSKI:def 1;

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

hence x in {g} * {h} by A3; :: thesis: verum

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

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

proof

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

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

then consider g1, g2 being Element of G such that

A1: x = g1 * g2 and

A2: ( g1 in {g} & g2 in {h} ) ;

( g1 = g & g2 = h ) by A2, TARSKI:def 1;

hence x in {(g * h)} by A1, TARSKI:def 1; :: thesis: verum

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

then consider g1, g2 being Element of G such that

A1: x = g1 * g2 and

A2: ( g1 in {g} & g2 in {h} ) ;

( g1 = g & g2 = h ) by A2, TARSKI:def 1;

hence x in {(g * h)} by A1, TARSKI:def 1; :: thesis: verum

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

then A3: x = g * h by TARSKI:def 1;

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

hence x in {g} * {h} by A3; :: thesis: verum