:: deftheorem Def1 defines vector RLVECT_2:def 1 :
for S being 1-sorted
for x being set st x in S holds
vector (S,x) = x;