let MS be non void 1 -element segmental ManySortedSign ; :: thesis: for i being OperSymbol of MS
for A being non-empty MSAlgebra over MS holds Args (i,A) c= (the_sort_of A) *
let i be OperSymbol of MS; :: thesis: for A being non-empty MSAlgebra over MS holds Args (i,A) c= (the_sort_of A) *
let A be non-empty MSAlgebra over MS; :: thesis: Args (i,A) c= (the_sort_of A) *
Args (i,A) = (len (the_arity_of i)) -tuples_on (the_sort_of A) by Th6;
hence Args (i,A) c= (the_sort_of A) * by FINSEQ_2:142; :: thesis: verum