take (1. F_Complex) * (1_. F_Complex) ; :: thesis: (1. F_Complex) * (1_. F_Complex) is Hurwitz
thus (1. F_Complex) * (1_. F_Complex) is Hurwitz by HURWITZ:38; :: thesis: verum