:: deftheorem defines prod_ZERO PRVECT_3:def 3 :
for G, F being non empty addLoopStr holds prod_ZERO (G,F) = [(0. G),(0. F)];