let G be non empty multMagma ; :: thesis: for A, B being Subset of G holds

( ( A <> {} & B <> {} ) iff A * B <> {} )

let A, B be Subset of G; :: thesis: ( ( A <> {} & B <> {} ) iff A * B <> {} )

thus ( A <> {} & B <> {} implies A * B <> {} ) :: thesis: ( A * B <> {} implies ( A <> {} & B <> {} ) )

assume A * B <> {} ; :: thesis: ( A <> {} & B <> {} )

then ex a, b being Element of G st

( the Element of A * B = a * b & a in A & b in B ) by Th8;

hence ( A <> {} & B <> {} ) ; :: thesis: verum

( ( A <> {} & B <> {} ) iff A * B <> {} )

let A, B be Subset of G; :: thesis: ( ( A <> {} & B <> {} ) iff A * B <> {} )

thus ( A <> {} & B <> {} implies A * B <> {} ) :: thesis: ( A * B <> {} implies ( A <> {} & B <> {} ) )

proof

set x = the Element of A * B;
assume A1:
A <> {}
; :: thesis: ( not B <> {} or A * B <> {} )

then reconsider x = the Element of A as Element of G by TARSKI:def 3;

assume A2: B <> {} ; :: thesis: A * B <> {}

then reconsider y = the Element of B as Element of G by TARSKI:def 3;

x * y in A * B by A1, A2;

hence A * B <> {} ; :: thesis: verum

end;then reconsider x = the Element of A as Element of G by TARSKI:def 3;

assume A2: B <> {} ; :: thesis: A * B <> {}

then reconsider y = the Element of B as Element of G by TARSKI:def 3;

x * y in A * B by A1, A2;

hence A * B <> {} ; :: thesis: verum

assume A * B <> {} ; :: thesis: ( A <> {} & B <> {} )

then ex a, b being Element of G st

( the Element of A * B = a * b & a in A & b in B ) by Th8;

hence ( A <> {} & B <> {} ) ; :: thesis: verum