let n be non zero Nat; :: thesis:
let D be n -element FinSequence; :: thesis:
let f be PartFunc of (product ((Seg n) --> RNS_Real)),RNS_Real; :: thesis:
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:
set I = CarProd ((Seg n) --> RNS_Real);
set I0 = CarProd ((Seg n) --> REAL);
consider CX being non-empty n -element FinSequence such that
A4: ( CX = carr ((Seg n) --> RNS_Real) & CarProduct CX = the carrier of (CarProduct ((Seg n) --> RNS_Real)) & CarProd ((Seg n) --> RNS_Real) = CarProd CX & CarProd ((Seg n) --> RNS_Real) is bijective ) by MEASUR15:def 7;
A5: dom (CarProd ((Seg n) --> RNS_Real)) = the carrier of (CarProduct ((Seg n) --> RNS_Real)) by FUNCT_2:def 1;
n |-> RNS_Real = (Seg n) --> RNS_Real by FINSEQ_2:def 2;
then the carrier of (product ((Seg n) --> RNS_Real)) = the carrier of (REAL-NS n) by LOPBAN15:11;
then the carrier of (product ((Seg n) --> RNS_Real)) = REAL n by REAL_NS1:def 4;
then rng (CarProd ((Seg n) --> RNS_Real)) = REAL n by A4, FUNCT_2:def 3;
then ( dom ((CarProd ((Seg n) --> RNS_Real)) ") = REAL n & rng ((CarProd ((Seg n) --> RNS_Real)) ") = the carrier of (CarProduct ((Seg n) --> RNS_Real)) ) by A4, A5, FUNCT_1:33;
then reconsider J = (CarProd ((Seg n) --> RNS_Real)) " as Function of (REAL n), the carrier of (CarProduct ((Seg n) --> RNS_Real)) by FUNCT_2:1;
reconsider F = f * (CarProd ((Seg n) --> RNS_Real)) as PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real ;
reconsider G = F as PartFunc of (CarProduct ((Seg n) --> REAL)),REAL by MEASUR15:42;
reconsider H = (R_EAL G) * J as PartFunc of (REAL n),ExtREAL ;
CarProduct D is Subset of (CarProduct ((Seg n) --> REAL)) by A1, FINSEQ_1:3, Th11;
then CarProduct D c= CarProduct ((Seg n) --> REAL) ;
then A6: CarProduct D c= the carrier of (CarProduct ((Seg n) --> RNS_Real)) by MEASUR15:42;
for x being object holds
( x in product D iff x in (CarProd ((Seg n) --> RNS_Real)) .: (CarProduct D) )

let x be object ; :: thesis:

hereby :: thesis:

assume A7: x in product D ; :: thesis:
then consider g being Function such that
A8: ( x = g & dom g = dom D & ( for y being object st y in dom D holds
g . y in D . y ) ) by CARD_3:def 5;
A9: dom D = Seg (len D) by FINSEQ_1:def 3;
then A10: dom D = Seg n by CARD_1:def 7;
reconsider t = x as FinSequence by A8, A9, FINSEQ_1:def 2;
Seg (len t) = Seg n by A8, A10, FINSEQ_1:def 3;
then reconsider y = t as n -element FinSequence by CARD_1:def 7, FINSEQ_1:6;
A11: PtCarProduct y in CarProduct D by A7, Th7;
reconsider s = PtCarProduct y as Point of (CarProduct ((Seg n) --> RNS_Real)) by A6, A7, Th7;
consider px being n -element FinSequence such that
A12: ( s = PtCarProduct px & (CarProd ((Seg n) --> RNS_Real)) . s = px ) by MEASUR15:28;
px = x by A12, MEASUR15:5;
hence x in (CarProd ((Seg n) --> RNS_Real)) .: (CarProduct D) by A5, A11, A12, FUNCT_1:def 6; :: thesis:

end;

assume x in (CarProd ((Seg n) --> RNS_Real)) .: (CarProduct D) ; :: thesis:
then consider t being object such that
A13: ( t in dom (CarProd ((Seg n) --> RNS_Real)) & t in CarProduct D & x = (CarProd ((Seg n) --> RNS_Real)) . t ) by FUNCT_1:def 6;
reconsider s = t as Point of (CarProduct ((Seg n) --> RNS_Real)) by A13;
consider px being n -element FinSequence such that
A14: ( s = PtCarProduct px & (CarProd ((Seg n) --> RNS_Real)) . s = px ) by MEASUR15:28;
ex qx being n -element FinSequence st
( qx in product D & t = PtCarProduct qx ) by A13, Th7;
hence x in product D by A13, A14, MEASUR15:5; :: thesis:

end;

then A15: product D = (CarProd ((Seg n) --> RNS_Real)) .: (CarProduct D) by TARSKI:2;
A16: CarProduct D c= dom (CarProd ((Seg n) --> RNS_Real)) by FUNCT_2:def 1, A6;
dom F = (CarProd ((Seg n) --> RNS_Real)) " (product D) by A3, RELAT_1:147;
then A17: dom F = CarProduct D by A15, FUNCT_1:94, A4, A16;
for x0 being Point of (CarProduct ((Seg n) --> RNS_Real))
for r being Real st x0 in CarProduct D & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in CarProduct D & ||.(x1 - x0).|| < s holds
||.((F /. x1) - (F /. x0)).|| < r ) )

let x0 be Point of (CarProduct ((Seg n) --> RNS_Real)); :: thesis:
let r be Real; :: thesis:
assume that
A18: x0 in CarProduct D and
A19: 0 < r ; :: thesis:
reconsider y0 = (CarProd ((Seg n) --> RNS_Real)) . x0 as Point of (product ((Seg n) --> RNS_Real)) ;
A20: y0 in product D by A5, A15, A18, FUNCT_1:def 6;
then consider s being Real such that
A21: ( 0 < s & ( for y1 being Point of (product ((Seg n) --> RNS_Real)) st y1 in product D & ||.(y1 - y0).|| < s holds
||.((f /. y1) - (f /. y0)).|| < r ) ) by A2, A3, A19, NFCONT_1:19;
take s ; :: thesis:
thus 0 < s by A21; :: thesis:
let x1 be Point of (CarProduct ((Seg n) --> RNS_Real)); :: thesis:
assume that
A22: x1 in CarProduct D and
A23: ||.(x1 - x0).|| < s ; :: thesis:
reconsider y1 = (CarProd ((Seg n) --> RNS_Real)) . x1 as Point of (product ((Seg n) --> RNS_Real)) ;
A24: y1 in product D by A5, A15, A22, FUNCT_1:def 6;
A25: - 1 is Element of REAL by XREAL_0:def 1;
y1 - y0 = y1 + ((- 1) * y0) by RLVECT_1:16;
then y1 - y0 = ((CarProd ((Seg n) --> RNS_Real)) . x1) + ((CarProd ((Seg n) --> RNS_Real)) . ((- 1) * x0)) by A25, MEASUR15:30;
then y1 - y0 = (CarProd ((Seg n) --> RNS_Real)) . (x1 + ((- 1) * x0)) by MEASUR15:29;
then y1 - y0 = (CarProd ((Seg n) --> RNS_Real)) . (x1 - x0) by RLVECT_1:16;
then ||.(x1 - x0).|| = ||.(y1 - y0).|| by MEASUR15:31;
then A26: ||.((f /. y1) - (f /. y0)).|| < r by A21, A23, A24;
F /. x1 = F . x1 by A17, PARTFUN1:def 6, A22;
then F /. x1 = f . ((CarProd ((Seg n) --> RNS_Real)) . x1) by A5, FUNCT_1:13;
then A27: F /. x1 = f /. y1 by A3, A24, PARTFUN1:def 6;
F /. x0 = F . x0 by A17, PARTFUN1:def 6, A18;
then F /. x0 = f . ((CarProd ((Seg n) --> RNS_Real)) . x0) by A5, FUNCT_1:13;
hence ||.((F /. x1) - (F /. x0)).|| < r by A26, A27, A3, A20, PARTFUN1:def 6; :: thesis:

end;

hence f * (CarProd ((Seg n) --> RNS_Real)) is_continuous_on CarProduct D by A17, NFCONT_1:19; :: thesis: