let G be non empty multMagma ; :: thesis: for A, B, C being Subset of G holds (A /\ B) * C c= (A * C) /\ (B * C)
let A, B, C be Subset of G; :: thesis: (A /\ B) * C c= (A * C) /\ (B * C)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A /\ B) * C or x in (A * C) /\ (B * C) )
assume x in (A /\ B) * C ; :: thesis: x in (A * C) /\ (B * C)
then consider g1, g2 being Element of G such that
A1: ( x = g1 * g2 & g1 in A /\ B & g2 in C ) ;
( g1 in A & g1 in B ) by A1, XBOOLE_0:def 4;
then ( x in A * C & x in B * C ) by A1;
hence x in (A * C) /\ (B * C) by XBOOLE_0:def 4; :: thesis: verum