:: deftheorem defines [: PRVECT_4:def 1 :
for E, F, G being non empty addLoopStr holds [:E,F,G:] = [:[:E,F:],G:];