let A, B be complex-membered set ; :: thesis: for a being Complex st a <> 0 holds
a ** (A /\ B) = (a ** A) /\ (a ** B)
let a be Complex; :: thesis: ( a <> 0 implies a ** (A /\ B) = (a ** A) /\ (a ** B) )
assume A1: a <> 0 ; :: thesis: a ** (A /\ B) = (a ** A) /\ (a ** B)
A2: (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 A3: 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
A4: z = a * c and
A5: c in A by Th195;
z in a ** B by A3, XBOOLE_0:def 4;
then consider c1 being Complex such that
A6: z = a * c1 and
A7: c1 in B by Th195;
c = c1 by A1, A4, A6, XCMPLX_1:5;
then c in A /\ B by A5, A7, XBOOLE_0:def 4;
hence z in a ** (A /\ B) by A4, Th193; :: thesis: verum

end;

a ** (A /\ B) c= (a ** A) /\ (a ** B) by Th93;
hence a ** (A /\ B) = (a ** A) /\ (a ** B) by A2; :: thesis: verum