let R be non trivial good Ring; :: thesis: for i, j being Element of NAT st i <> j holds
dl. (R,i) <> dl. (R,j)
let i, j be Element of NAT ; :: thesis: ( i <> j implies dl. (R,i) <> dl. (R,j) )
assume A1: i <> j ; :: thesis: dl. (R,i) <> dl. (R,j)
( dl. (R,j) = [1,j] & dl. (R,i) = [1,i] ) by Th2;
hence dl. (R,i) <> dl. (R,j) by A1, ZFMISC_1:27; :: thesis: verum