theorem :: FINSEQ_3:45

for m, n being Nat st 0 < n & n < m holds
Sgm {n,m} = <*n,m*>