let B, C be complex-membered set ; :: thesis: for a being Complex holds a ** (B ++ C) = (a ** B) ++ (a ** C)
let a be Complex; :: thesis: a ** (B ++ C) = (a ** B) ++ (a ** C)
A1: (a ** B) ++ (a ** C) c= a ** (B ++ C)

proof

let z be Complex; :: according to MEMBERED:def 7 :: thesis: ( not z in (a ** B) ++ (a ** C) or z in a ** (B ++ C) )
assume z in (a ** B) ++ (a ** C) ; :: thesis: z in a ** (B ++ C)
then consider c, c1 being Complex such that
A2: z = c + c1 and
A3: c in a ** B and
A4: c1 in a ** C ;
consider c3 being Complex such that
A5: c1 = a * c3 and
A6: c3 in C by A4, Th195;
consider c2 being Complex such that
A7: c = a * c2 and
A8: c2 in B by A3, Th195;
A9: c2 + c3 in B ++ C by A8, A6;
z = a * (c2 + c3) by A2, A7, A5;
hence z in a ** (B ++ C) by A9, Th193; :: thesis: verum

end;

a ** (B ++ C) c= (a ** B) ++ (a ** C) by Th95;
hence a ** (B ++ C) = (a ** B) ++ (a ** C) by A1; :: thesis: verum