let S be non empty non void ManySortedSign ; :: thesis: for A, B being non-empty disjoint_valued MSAlgebra over S
for C being non-empty MSAlgebra over S
for f being ManySortedFunction of A,B
for g being ManySortedFunction of B,C
for a being Element of A holds (g ** f) . a = g . (f . a)
let A, B be non-empty disjoint_valued MSAlgebra over S; :: thesis: for C being non-empty MSAlgebra over S
for f being ManySortedFunction of A,B
for g being ManySortedFunction of B,C
for a being Element of A holds (g ** f) . a = g . (f . a)
let C be non-empty MSAlgebra over S; :: thesis: for f being ManySortedFunction of A,B
for g being ManySortedFunction of B,C
for a being Element of A holds (g ** f) . a = g . (f . a)
let f be ManySortedFunction of A,B; :: thesis: for g being ManySortedFunction of B,C
for a being Element of A holds (g ** f) . a = g . (f . a)
let g be ManySortedFunction of B,C; :: thesis: for a being Element of A holds (g ** f) . a = g . (f . a)
let a be Element of A; :: thesis: (g ** f) . a = g . (f . a)
A1: ( a in the Sorts of A . (the_sort_of a) & f . (the_sort_of a) is Function of ( the Sorts of A . (the_sort_of a)),( the Sorts of B . (the_sort_of a)) ) by SORT;
thus (g ** f) . a = ((g ** f) . (the_sort_of a)) . a by ABBR
.= ((g . (the_sort_of a)) * (f . (the_sort_of a))) . a by MSUALG_3:2
.= (g . (the_sort_of a)) . ((f . (the_sort_of a)) . a) by A1, FUNCT_2:15
.= (g . (the_sort_of (f . a))) . ((f . (the_sort_of a)) . a) by Lem0
.= (g . (the_sort_of (f . a))) . (f . a) by ABBR
.= g . (f . a) by ABBR ; :: thesis: verum