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