let n be Nat; :: thesis: for X being RealNormSpace-Sequence st X = n |-> RNS_Real holds
( product X is finite-dimensional & dim (product X) = n )
let X be RealNormSpace-Sequence; :: thesis: ( X = n |-> RNS_Real implies ( product X is finite-dimensional & dim (product X) = n ) )
assume X = n |-> RNS_Real ; :: thesis: ( product X is finite-dimensional & dim (product X) = n )
then product X = REAL-NS n by Th13;
hence ( product X is finite-dimensional & dim (product X) = n ) by REAL_NS2:62; :: thesis: verum