let a be Element of Args (o,A); :: thesis: ( a is Function-like & a is Relation-like )
dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
then Args (o,A) = ( the Sorts of A #) . (the_arity_of o) by FUNCT_1:13
.= product ( the Sorts of A * (the_arity_of o)) by FINSEQ_2:def 5 ;
hence ( a is Function-like & a is Relation-like ) ; :: thesis: verum