let MS be non empty trivial non void segmental ManySortedSign ; :: thesis: for i being OperSymbol of MS
for A being non-empty MSAlgebra of MS holds Args i,A c= (the_sort_of A) *
let i be OperSymbol of MS; :: thesis: for A being non-empty MSAlgebra of MS holds Args i,A c= (the_sort_of A) *
let A be non-empty MSAlgebra of 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 Th11;
hence Args i,A c= (the_sort_of A) * by FINSEQ_2:162; :: thesis: verum