let n be Nat; :: thesis: (Partial_Product (seq_const 0c)) . n = 0
(NAT --> 0) . n = 0 ;
then (Partial_Product (seq_const 0)) . (0 + n) = 0 by PPM;
hence (Partial_Product (seq_const 0c)) . n = 0 ; :: thesis: verum