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 Th43
.= g * (f * (id X)) by Th47
.= (g * f) * (id X) by RELAT_1:55 ;
:: thesis: verum