let n be non zero Nat; :: thesis: ( REAL-NS n = product ((Seg n) --> RNS_Real) & REAL n = the carrier of (product ((Seg n) --> RNS_Real)) & REAL n = product ((Seg n) --> REAL) )
A1: n |-> RNS_Real = (Seg n) --> RNS_Real by FINSEQ_2:def 2;
hence REAL-NS n = product ((Seg n) --> RNS_Real) by LOPBAN15:11; :: thesis: ( REAL n = the carrier of (product ((Seg n) --> RNS_Real)) & REAL n = product ((Seg n) --> REAL) )
the carrier of (product ((Seg n) --> RNS_Real)) = the carrier of (REAL-NS n) by A1, LOPBAN15:11;
hence REAL n = the carrier of (product ((Seg n) --> RNS_Real)) by REAL_NS1:def 4; :: thesis: REAL n = product ((Seg n) --> REAL)
product ((Seg n) --> REAL) = n -tuples_on REAL by SRINGS_5:10;
hence product ((Seg n) --> REAL) = REAL n by EUCLID:def 1; :: thesis: verum