now :: thesis: for n being positive Nat holds n '*' (1. F_Complex) <> 0. F_Complex

let n be positive Nat; :: thesis: n '*' (1. F_Complex) <> 0. F_Complex
n '*' (1. F_Complex) = n by Lm9;
hence n '*' (1. F_Complex) <> 0. F_Complex by COMPLFLD:def 1; :: thesis: verum

end;

hence F_Complex is 0 -characteristic by Def5; :: thesis: verum