let G be RealNormSpace-Sequence; :: thesis: the carrier of (product G) = product (carr G)
product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by PRVECT_2:6;
hence the carrier of (product G) = product (carr G) ; :: thesis: verum