let A, B, C be complex-membered set ; :: thesis: A ** (B /\ C) c= (A ** B) /\ (A ** C)
let a be Complex; :: according to MEMBERED:def 7 :: thesis: ( not a in A ** (B /\ C) or a in (A ** B) /\ (A ** 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 C by A3, XBOOLE_0:def 4;
then A4: c * c1 in A ** C by A2;
c1 in B by A3, XBOOLE_0:def 4;
then c * c1 in A ** B by A2;
hence a in (A ** B) /\ (A ** C) by A1, A4, XBOOLE_0:def 4; :: thesis: verum