reconsider G0 = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) as non empty strict NORMSTR ;
take
G0
; ( RLSStruct(# the carrier of G0, the ZeroF of G0, the addF of G0, the Mult of G0 #) = product G & the normF of G0 = productnorm G )
thus
( RLSStruct(# the carrier of G0, the ZeroF of G0, the addF of G0, the Mult of G0 #) = product G & the normF of G0 = productnorm G )
; verum