let L be domRing; :: thesis: for n being non zero Nat
for a being non zero Element of L st Char L = 0 holds
n * a <> 0. L
let n be non zero Nat; :: thesis: for a being non zero Element of L st Char L = 0 holds
n * a <> 0. L
let a be non zero Element of L; :: thesis: ( Char L = 0 implies n * a <> 0. L )
n * a = n '*' a by RING_3:def 2;
hence ( Char L = 0 implies n * a <> 0. L ) by REALALG2:25; :: thesis: verum