let n be non zero Nat; :: thesis: for D being n -element FinSequence
for f being PartFunc of (REAL-NS n),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
let D be n -element FinSequence; :: thesis: for f being PartFunc of (REAL-NS n),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
let f be PartFunc of (REAL-NS n),RNS_Real; :: thesis: ( ( 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 implies f * (CarProd ((Seg n) --> RNS_Real)) is_continuous_on CarProduct D )
assume that
A1: for i being Nat st i in Seg n holds
D . i is Subset of REAL and
A2: f is_continuous_on dom f and
A3: dom f = product D ; :: thesis: f * (CarProd ((Seg n) --> RNS_Real)) is_continuous_on CarProduct D
reconsider f1 = f as PartFunc of (product ((Seg n) --> RNS_Real)),RNS_Real by Th61;
f1 is_continuous_on dom f1 by A2, Th61;
hence f * (CarProd ((Seg n) --> RNS_Real)) is_continuous_on CarProduct D by A1, A3, Th60; :: thesis: verum