theorem :: MESFUN18:59

for n being non zero Nat
for f being PartFunc of (product ((Seg n) --> RNS_Real)),RNS_Real holds f * (CarProd ((Seg n) --> RNS_Real)) is PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real ;