let X be set ; for f, g, h being Function holds compose (<*f,g,h*>,X) = ((h * g) * f) * (id X)
let f, g, h be Function; 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
;
verum