for x1, x2 being Real holds cpx2euc (x1 + (x2 * <i>)) = |[x1,x2]|