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) = {} )

A1: now

consider x being Element of A * ({} the carrier of G);
assume A * ({} the carrier of G) <> {} ; :: thesis: contradiction
then ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in A & g2 in {} the carrier of G ) by Th12;
hence contradiction ; :: thesis: verum

end;

now

consider x being Element of ({} the carrier of G) * A;
assume ({} the carrier of G) * A <> {} ; :: thesis: contradiction
then ex g1, g2 being Element of G st
( x = g1 * g2 & g1 in {} the carrier of G & g2 in A ) by Th12;
hence contradiction ; :: thesis: verum

end;

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