let G be non empty multMagma ; :: thesis: for A, B, C being Subset of G holds (A \/ B) * C = (A * C) \/ (B * C)

let A, B, C be Subset of G; :: thesis: (A \/ B) * C = (A * C) \/ (B * C)

thus (A \/ B) * C c= (A * C) \/ (B * C) :: according to XBOOLE_0:def 10 :: thesis: (A * C) \/ (B * C) c= (A \/ B) * C

assume A4: x in (A * C) \/ (B * C) ; :: thesis: x in (A \/ B) * C

let A, B, C be Subset of G; :: thesis: (A \/ B) * C = (A * C) \/ (B * C)

thus (A \/ B) * C c= (A * C) \/ (B * C) :: according to XBOOLE_0:def 10 :: thesis: (A * C) \/ (B * C) c= (A \/ B) * C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A * C) \/ (B * C) or x in (A \/ B) * C )
let x be object ; :: 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 and

A2: g1 in A \/ B and

A3: g2 in C ;

( g1 in A or g1 in B ) by A2, XBOOLE_0:def 3;

then ( x in A * C or x in B * C ) by A1, A3;

hence x in (A * C) \/ (B * C) by XBOOLE_0:def 3; :: thesis: verum

end;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 and

A2: g1 in A \/ B and

A3: g2 in C ;

( g1 in A or g1 in B ) by A2, XBOOLE_0:def 3;

then ( x in A * C or x in B * C ) by A1, A3;

hence x in (A * C) \/ (B * C) by XBOOLE_0:def 3; :: thesis: verum

assume A4: x in (A * C) \/ (B * C) ; :: thesis: x in (A \/ B) * C

now :: thesis: x in (A \/ B) * Cend;

hence
x in (A \/ B) * C
; :: thesis: verumper cases
( x in A * C or x in B * C )
by A4, XBOOLE_0:def 3;

end;