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:60;
hence compose <*f,g,h*>,X = h * (compose <*f,g*>,X) by Th43
.= h * ((g * f) * (id X)) by Th53
.= (h * (g * f)) * (id X) by RELAT_1:55
.= ((h * g) * f) * (id X) by RELAT_1:55 ;
:: thesis: verum