let v be Element of ; :: 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