for f being FinSequence of COMPLEX holds XProduct (FS2XFS f) = Product f