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 Th40
.= f * (id X) by Th38 ;
:: thesis: verum