let n be non zero Nat; :: thesis: for D being n -element FinSequence st ( for i being Nat st i in Seg n holds
D . i c= REAL ) holds
product D = (CarProd ((Seg n) --> REAL)) .: (CarProduct D)
let D be n -element FinSequence; :: thesis: ( ( for i being Nat st i in Seg n holds
D . i c= REAL ) implies product D = (CarProd ((Seg n) --> REAL)) .: (CarProduct D) )
assume A1: for i being Nat st i in Seg n holds
D . i c= REAL ; :: thesis: product D = (CarProd ((Seg n) --> REAL)) .: (CarProduct D)
set I = CarProd ((Seg n) --> RNS_Real);
A2: dom (CarProd ((Seg n) --> RNS_Real)) = the carrier of (CarProduct ((Seg n) --> RNS_Real)) by FUNCT_2:def 1;
A3: CarProduct D c= the carrier of (CarProduct ((Seg n) --> RNS_Real))

proof

per cases ( D is non-empty or not D is non-empty ) ;

suppose D is non-empty ; :: thesis: CarProduct D c= the carrier of (CarProduct ((Seg n) --> RNS_Real))

then reconsider D1 = D as non-empty n -element FinSequence ;
CarProduct D1 c= CarProduct ((Seg n) --> REAL) by A1, MEASUR15:34;
hence CarProduct D c= the carrier of (CarProduct ((Seg n) --> RNS_Real)) by MEASUR15:42; :: thesis: verum

end;

suppose not D is non-empty ; :: thesis: CarProduct D c= the carrier of (CarProduct ((Seg n) --> RNS_Real))

hence CarProduct D c= the carrier of (CarProduct ((Seg n) --> RNS_Real)) by Th6; :: thesis: verum

end;

end;

end;

for x being object holds
( x in product D iff x in (CarProd ((Seg n) --> RNS_Real)) .: (CarProduct D) )

proof

let x be object ; :: thesis: ( x in product D iff x in (CarProd ((Seg n) --> RNS_Real)) .: (CarProduct D) )

hereby :: thesis: ( x in (CarProd ((Seg n) --> RNS_Real)) .: (CarProduct D) implies x in product D )

assume A4: x in product D ; :: thesis: x in (CarProd ((Seg n) --> RNS_Real)) .: (CarProduct D)
then consider g being Function such that
A5: ( 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;
A6: dom D = Seg (len D) by FINSEQ_1:def 3;
then reconsider t = x as FinSequence by A5, FINSEQ_1:def 2;
dom D = Seg n by A6, CARD_1:def 7;
then Seg (len t) = Seg n by A5, FINSEQ_1:def 3;
then reconsider y = t as n -element FinSequence by FINSEQ_1:6, CARD_1:def 7;
A7: PtCarProduct y in CarProduct D by A4, Th7;
reconsider s = PtCarProduct y as Point of (CarProduct ((Seg n) --> RNS_Real)) by A3, A4, Th7;
consider px being n -element FinSequence such that
A8: ( s = PtCarProduct px & (CarProd ((Seg n) --> RNS_Real)) . s = px ) by MEASUR15:28;
px = y by A8, MEASUR15:5;
hence x in (CarProd ((Seg n) --> RNS_Real)) .: (CarProduct D) by A2, A7, A8, FUNCT_1:def 6; :: thesis: verum

end;

assume x in (CarProd ((Seg n) --> RNS_Real)) .: (CarProduct D) ; :: thesis: x in product D
then consider t being object such that
A9: ( 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 A9;
A10: ex px being n -element FinSequence st
( 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 A9, Th7;
hence x in product D by A9, A10, MEASUR15:5; :: thesis: verum

end;

then product D = (CarProd ((Seg n) --> RNS_Real)) .: (CarProduct D) by TARSKI:2;
hence product D = (CarProd ((Seg n) --> REAL)) .: (CarProduct D) by MEASUR15:70; :: thesis: verum