let R be domRing; :: thesis: ( Char R = 0 iff for a being non zero Element of R
for n being non zero Nat holds n '*' a <> 0. R )
hereby :: thesis: ( ( for a being non zero Element of R
for n being non zero Nat holds n '*' a <> 0. R ) implies Char R = 0 )
assume AS: Char R = 0 ; :: thesis: for a being non zero Element of R
for n being non zero Nat holds n '*' a <> 0. R
now :: thesis: for a being non zero Element of R
for n being non zero Nat holds not n '*' a = 0. R
given a being non zero Element of R, n being non zero Nat such that H: n '*' a = 0. R ; :: thesis: contradiction
0. R = n '*' ((1. R) * a) by H
.= (n '*' (1. R)) * a by c1 ;
then n '*' (1. R) = 0. R by VECTSP_2:def 1;
hence contradiction by AS, RING_3:def 5; :: thesis: verum
end;
hence for a being non zero Element of R
for n being non zero Nat holds n '*' a <> 0. R ; :: thesis: verum
end;
assume AS: for a being non zero Element of R
for n being non zero Nat holds n '*' a <> 0. R ; :: thesis: Char R = 0
now :: thesis: ( Char R <> 0 implies for x being Element of CharSet R holds contradiction )
assume Char R <> 0 ; :: thesis: for x being Element of CharSet R holds contradiction
then H1: CharSet R <> {} by RING_3:78;
let x be Element of CharSet R; :: thesis: contradiction
x in CharSet R by H1;
then ex n being positive Nat st
( x = n & n '*' (1. R) = 0. R ) ;
hence contradiction by AS; :: thesis: verum
end;
hence Char R = 0 ; :: thesis: verum