let X be set ; :: thesis: for f being Function holds compose <*f*>,X = f * (id X)
let f be Function; :: thesis: compose <*f*>,X = f * (id X)
<*f*> = {} ^ <*f*> by FINSEQ_1:47;
hence compose <*f*>,X = f * (compose {} ,X) by Th43
.= f * (id X) by Th41 ;
:: thesis: verum