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 ;
consider c2, c3 being Complex such that
A4: ( c1 = c2 + c3 & c2 in B ) and
A5: c3 in C by A3;
A6: c * c3 in A ** C by A2, A5;
( a = (c * c2) + (c * c3) & c * c2 in A ** B ) by A1, A2, A4;
hence a in (A ** B) ++ (A ** C) by A6; :: thesis: verum