let R be 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 Th3;
hence dl. R,i <> dl. R,j by A1, ZFMISC_1:33; :: thesis: verum