let S be non empty non void ManySortedSign ; :: thesis: for A, B being non-empty disjoint_valued MSAlgebra over S
for f being ManySortedFunction of A,B
for a being Element of A holds the_sort_of (f . a) = the_sort_of a
let A, B be non-empty disjoint_valued MSAlgebra over S; :: thesis: for f being ManySortedFunction of A,B
for a being Element of A holds the_sort_of (f . a) = the_sort_of a
let f be ManySortedFunction of A,B; :: thesis: for a being Element of A holds the_sort_of (f . a) = the_sort_of a
let a be Element of A; :: thesis: the_sort_of (f . a) = the_sort_of a
a in the Sorts of A . (the_sort_of a) by SORT;
then ( f . a = (f . (the_sort_of a)) . a & (f . (the_sort_of a)) . a in the Sorts of B . (the_sort_of a) ) by ABBR, FUNCT_2:5;
hence the_sort_of (f . a) = the_sort_of a by SORT; :: thesis: verum