let A, B be complex-membered set ; :: thesis: for a being complex number holds a ++ (A /\ B) = (a ++ A) /\ (a ++ B)
let a be complex number ; :: thesis: a ++ (A /\ B) = (a ++ A) /\ (a ++ B)
A1: (a ++ A) /\ (a ++ B) c= a ++ (A /\ B)

proof

let z be complex number ; :: according to MEMBERED:def 7 :: thesis: ( not z in (a ++ A) /\ (a ++ B) or z in a ++ (A /\ B) )
assume A2: z in (a ++ A) /\ (a ++ B) ; :: thesis: z in a ++ (A /\ B)
then z in a ++ A by XBOOLE_0:def 4;
then consider c being Element of COMPLEX such that
A3: z = a + c and
A4: c in A by Th143;
z in a ++ B by A2, XBOOLE_0:def 4;
then ex c1 being Element of COMPLEX st
( z = a + c1 & c1 in B ) by Th143;
then c in A /\ B by A3, A4, XBOOLE_0:def 4;
hence z in a ++ (A /\ B) by A3, Th141; :: thesis: verum

end;

a ++ (A /\ B) c= (a ++ A) /\ (a ++ B) by Th49;
hence a ++ (A /\ B) = (a ++ A) /\ (a ++ B) by A1, XBOOLE_0:def 10; :: thesis: verum