let n, i, j be Nat; :: thesis: ( [i,j] in [:(Seg n),(Seg n):] & i + j <> n + 1 implies ((i + j) - 1) mod n in Seg n )
assume that
A1: [i,j] in [:(Seg n),(Seg n):] and
A2: i + j <> n + 1 ; :: thesis: ((i + j) - 1) mod n in Seg n
( i in Seg n & j in Seg n ) by A1, ZFMISC_1:87;
hence ((i + j) - 1) mod n in Seg n by A2, Lm3; :: thesis: verum