(seq_const 0) . 0 = 0 ;
then 0 = (Partial_Product (seq_const 0)) . (0 + k) by PPM;
hence (Partial_Product (seq_const 0)) . k = 0 ; :: thesis: verum