let v be Element of (n -VectSp_over K); :: thesis: ( v is Function-like & v is Relation-like )
v is Element of n -tuples_on the carrier of K by Th102;
hence ( v is Function-like & v is Relation-like ) ; :: thesis: verum