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

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