let f, g be complex-valued FinSequence; :: thesis: Product (f ^ g) = (Product f) * (Product g)
Product (((f ^ g) | (len f)) ^ ((f ^ g) /^ (len f))) = (Product f) * (Product g) by PAP;
hence Product (f ^ g) = (Product f) * (Product g) ; :: thesis: verum