:: deftheorem defines Triangle NUMPOLY1:def 1 :
for n being Nat holds Triangle n = Sum (idseq n);