theorem :: RVSUM_4:59

for f being XFinSequence of COMPLEX
for g being FinSequence of COMPLEX holds
( XProduct (f ^ g) = (XProduct f) * (Product g) & Product (g ^ f) = (Product g) * (XProduct f) )