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;