let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for A being non-empty disjoint_valued MSAlgebra over S
for a being b₁ -sort Element of A holds the_sort_of a = s
let s be SortSymbol of S; :: thesis: for A being non-empty disjoint_valued MSAlgebra over S
for a being s -sort Element of A holds the_sort_of a = s
let A be non-empty disjoint_valued MSAlgebra over S; :: thesis: for a being s -sort Element of A holds the_sort_of a = s
let a be s -sort Element of A; :: thesis: the_sort_of a = s
a in the Sorts of A . s by AS;
hence the_sort_of a = s by SORT; :: thesis: verum