for n being Nat holds (Partial_Product (seq_const 0c)) . n = 0