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

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

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

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

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

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

proof

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

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

then consider g1, g2 being Element of G such that

A1: ( x = g1 * g2 & g1 in A ) and

A2: g2 in B \/ C ;

( g2 in B or g2 in C ) by A2, XBOOLE_0:def 3;

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

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

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

then consider g1, g2 being Element of G such that

A1: ( x = g1 * g2 & g1 in A ) and

A2: g2 in B \/ C ;

( g2 in B or g2 in C ) by A2, XBOOLE_0:def 3;

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

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

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

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

hence
x in A * (B \/ C)
; :: thesis: verumend;