:: deftheorem defines ! SIN_COS:def 3 :
for n being Nat holds n ! = Prod_real_n . n;