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