:: deftheorem defines real HURWITZ2:def 13 :
for Z being rational_function of F_Complex holds
( Z is real iff for i being Nat holds
( (Z `1) . i is Real & (Z `2) . i is Real ) );