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