Args (o,SCS) = product ( the Sorts of SCS * (the_arity_of o)) by PRALG_2:3;
hence s * (the_arity_of o) is Element of Args (o,SCS) by CARD_3:83; :: thesis: verum