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 is Element of the Sorts of B . s
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 is Element of the Sorts of B . s
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 is Element of the Sorts of B . s
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 is Element of the Sorts of B . s
let f be ManySortedFunction of A,B; :: thesis: for a being Element of the Sorts of A . s holds f . a is Element of the Sorts of B . s
let a be Element of the Sorts of A . s; :: thesis: f . a is Element of the Sorts of B . s
( f . a = (f . s) . a & (f . s) . a in the Sorts of B . s ) by Th9, FUNCT_2:5;
hence f . a is Element of the Sorts of B . s ; :: thesis: verum