let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T holds the_sort_of (@ r) = the_sort_of r
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T holds the_sort_of (@ r) = the_sort_of r
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for r being Element of T holds the_sort_of (@ r) = the_sort_of r
let r be Element of T; :: thesis: the_sort_of (@ r) = the_sort_of r
the Sorts of T is MSSubset of (Free (S,X)) by MSAFREE4:def 6;
then ( @ r in the Sorts of T . (the_sort_of r) & the Sorts of T . (the_sort_of r) c= the Sorts of (Free (S,X)) . (the_sort_of r) ) by SORT, PBOOLE:def 2, PBOOLE:def 18;
hence the_sort_of (@ r) = the_sort_of r by SORT; :: thesis: verum