let X be set ; :: thesis: for f, g, h being Function holds compose (<*f,g,h*>,X) = ((h * g) * f) * (id X)
let f, g, h be Function; :: thesis: compose (<*f,g,h*>,X) = ((h * g) * f) * (id X)
<*f,g,h*> = <*f,g*> ^ <*h*> by FINSEQ_1:43;
hence compose (<*f,g,h*>,X) = h * (compose (<*f,g*>,X)) by Th40
.= h * ((g * f) * (id X)) by Th50
.= (h * (g * f)) * (id X) by RELAT_1:36
.= ((h * g) * f) * (id X) by RELAT_1:36 ;
:: thesis: verum