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