for n being Nat holds
( 0 ! = 1 & n ! <> 0 & (n + 1) ! = (n !) * (n + 1) ) by Def2;