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 B being non-empty MSAlgebra over S
for f being ManySortedFunction of A,B
for a being Element of the Sorts of A . s holds f . a = (f . s) . a
let s be SortSymbol of S; :: thesis: for A being non-empty disjoint_valued MSAlgebra over S
for B being non-empty MSAlgebra over S
for f being ManySortedFunction of A,B
for a being Element of the Sorts of A . s holds f . a = (f . s) . a
let A be non-empty disjoint_valued MSAlgebra over S; :: thesis: for B being non-empty MSAlgebra over S
for f being ManySortedFunction of A,B
for a being Element of the Sorts of A . s holds f . a = (f . s) . a
let B be non-empty MSAlgebra over S; :: thesis: for f being ManySortedFunction of A,B
for a being Element of the Sorts of A . s holds f . a = (f . s) . a
let f be ManySortedFunction of A,B; :: thesis: for a being Element of the Sorts of A . s holds f . a = (f . s) . a
let a be Element of the Sorts of A . s; :: thesis: f . a = (f . s) . a
thus f . a = (f . (the_sort_of a)) . a by ABBR
.= (f . s) . a by SORT ; :: thesis: verum