( a #Z k = a |^ |.k.| or a #Z k = (a |^ |.k.|) " ) by Def3;
hence a #Z k is real ; :: thesis: verum