let A, B be complex-membered set ; :: thesis: for a being Complex holds a ++ (A /\ B) = (a ++ A) /\ (a ++ B)
let a be Complex; :: thesis: a ++ (A /\ B) = (a ++ A) /\ (a ++ B)
A1: (a ++ A) /\ (a ++ B) c= a ++ (A /\ B)
proof
let z be Complex; :: 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 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 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; :: thesis: verum