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

( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} )

let A be Subset of G; :: thesis: ( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} )

( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} )

let A be Subset of G; :: thesis: ( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} )

A1: now :: thesis: not A * ({} the carrier of G) <> {}

set x = the Element of A * ({} the carrier of G);

assume A * ({} the carrier of G) <> {} ; :: thesis: contradiction

then ex g1, g2 being Element of G st

( the Element of A * ({} the carrier of G) = g1 * g2 & g1 in A & g2 in {} the carrier of G ) by Th8;

hence contradiction ; :: thesis: verum

end;assume A * ({} the carrier of G) <> {} ; :: thesis: contradiction

then ex g1, g2 being Element of G st

( the Element of A * ({} the carrier of G) = g1 * g2 & g1 in A & g2 in {} the carrier of G ) by Th8;

hence contradiction ; :: thesis: verum

now :: thesis: not ({} the carrier of G) * A <> {}

hence
( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} )
by A1; :: thesis: verumset x = the Element of ({} the carrier of G) * A;

assume ({} the carrier of G) * A <> {} ; :: thesis: contradiction

then ex g1, g2 being Element of G st

( the Element of ({} the carrier of G) * A = g1 * g2 & g1 in {} the carrier of G & g2 in A ) by Th8;

hence contradiction ; :: thesis: verum

end;assume ({} the carrier of G) * A <> {} ; :: thesis: contradiction

then ex g1, g2 being Element of G st

( the Element of ({} the carrier of G) * A = g1 * g2 & g1 in {} the carrier of G & g2 in A ) by Th8;

hence contradiction ; :: thesis: verum