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

assume A2: ({} the carrier of G) * A <> {} ; :: thesis: contradiction
consider x being Element of ({} the carrier of G) * A;
consider g1, g2 being Element of G such that
x = g1 * g2 and
A3: g1 in {} the carrier of G and
g2 in A by A2, Th12;
thus contradiction by A3; :: thesis: verum

end;

now

assume A4: A * ({} the carrier of G) <> {} ; :: thesis: contradiction
consider x being Element of A * ({} the carrier of G);
consider g1, g2 being Element of G such that
x = g1 * g2 and
g1 in A and
A5: g2 in {} the carrier of G by A4, Th12;
thus contradiction by A5; :: thesis: verum

end;

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