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 :: 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;
now :: thesis: not ({} the carrier of G) * A <> {}
set 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;
hence ( ({} the carrier of G) * A = {} & A * ({} the carrier of G) = {} ) by A1; :: thesis: verum