let a be Complex; :: thesis: a = |.a.| * (director a)

per cases ( a is zero or not a is zero ) ;

suppose a is zero ; :: thesis: a = |.a.| * (director a)

hence a = |.a.| * (director a) ; :: thesis: verum

end;

suppose not a is zero ; :: thesis: a = |.a.| * (director a)

hence a = |.a.| * (director a) by XCMPLX_1:87; :: thesis: verum

end;

end;