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