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

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