let R be non trivial Ring; :: thesis: for i, j being Nat st i <> j holds
dl. (R,i) <> dl. (R,j)
let i, j be 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 Th1;
hence dl. (R,i) <> dl. (R,j) by A1, XTUPLE_0:1; :: thesis: verum