let A, B, C be complex-membered set ; :: thesis: A ** (B \/ C) = (A ** B) \/ (A ** C)
let a be Complex; :: according to MEMBERED:def 13 :: thesis: ( ( not a in A ** (B \/ C) or a in (A ** B) \/ (A ** C) ) & ( not a in (A ** B) \/ (A ** C) or a in A ** (B \/ C) ) )

hereby :: thesis: ( not a in (A ** B) \/ (A ** C) or a in A ** (B \/ C) )

assume a in A ** (B \/ C) ; :: thesis: a in (A ** B) \/ (A ** C)
then consider c, c1 being Complex such that
A1: a = c * c1 and
A2: c in A and
A3: c1 in B \/ C ;
( c1 in B or c1 in C ) by A3, XBOOLE_0:def 3;
then ( c * c1 in A ** B or c * c1 in A ** C ) by A2;
hence a in (A ** B) \/ (A ** C) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

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

per cases ( a in A ** B or a in A ** C ) by A4, XBOOLE_0:def 3;

suppose a in A ** B ; :: thesis: a in A ** (B \/ C)

then consider c, c1 being Complex such that
A5: ( a = c * c1 & c in A ) and
A6: c1 in B ;
c1 in B \/ C by A6, XBOOLE_0:def 3;
hence a in A ** (B \/ C) by A5; :: thesis: verum

end;

suppose a in A ** C ; :: thesis: a in A ** (B \/ C)

then consider c, c1 being Complex such that
A7: ( a = c * c1 & c in A ) and
A8: c1 in C ;
c1 in B \/ C by A8, XBOOLE_0:def 3;
hence a in A ** (B \/ C) by A7; :: thesis: verum

end;

end;