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:34;
hence compose (<*f*>,X) = f * (compose ({},X)) by Th43
.= f * (id X) by Th41 ;
:: thesis: verum