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