reconsider G0 = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) as non empty strict NORMSTR ;
take G0 ; :: thesis: ( 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 ) ; :: thesis: verum