:: deftheorem defines ! NEWTON:def 2 :
for n being natural Number holds n ! = Product (idseq n);