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