let A, B, C be complex-membered set ; :: thesis: A ** (B ++ C) c= (A ** B) ++ (A ** C)
let a be complex number ; :: 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 Element of COMPLEX such that
A1: a = c * c1 and
A2: c in A and
A3: c1 in B ++ C ;
consider c2, c3 being Element of COMPLEX such that
A4: c1 = c2 + c3 and
A5: c2 in B and
A6: c3 in C by A3;
A7: a = (c * c2) + (c * c3) by A1, A4;
( c * c2 in A ** B & c * c3 in A ** C ) by A2, A5, A6;
hence a in (A ** B) ++ (A ** C) by A7; :: thesis: verum