for rseq being Real_Sequence
for cseq being Complex_Sequence st cseq = rseq holds
Partial_Product rseq = Partial_Product cseq