let a be Element of (product G); :: according to MONOID_0:def 2 :: thesis: a is set
product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by PRVECT_2:6;
hence a is set by Th9; :: thesis: verum