theorem Th60: :: MESFUN18:60

for n being non zero Nat
for D being b₁ -element FinSequence
for f being PartFunc of (product ((Seg n) --> RNS_Real)),RNS_Real st ( for i being Nat st i in Seg n holds
D . i is Subset of REAL ) & f is_continuous_on dom f & dom f = product D holds
f * (CarProd ((Seg n) --> RNS_Real)) is_continuous_on CarProduct D