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 norm 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 norm of G0 = productnorm G ) ; :: thesis: verum