let I be set ; :: thesis: for C being Category
for f being Morphism of C
for F being Function of I,the carrier' of C holds f * F = (I --> f) "*" F
let C be Category; :: thesis: for f being Morphism of C
for F being Function of I,the carrier' of C holds f * F = (I --> f) "*" F
let f be Morphism of C; :: thesis: for F being Function of I,the carrier' of C holds f * F = (I --> f) "*" F
let F be Function of I,the carrier' of C; :: thesis: f * F = (I --> f) "*" F

now

let x be set ; :: thesis: ( x in I implies (f * F) /. x = ((I --> f) "*" F) /. x )
assume A1: x in I ; :: thesis: (f * F) /. x = ((I --> f) "*" F) /. x
hence (f * F) /. x = f * (F /. x) by Def8
.= ((I --> f) /. x) * (F /. x) by A1, Th2
.= ((I --> f) "*" F) /. x by A1, Def9 ;
:: thesis: verum

end;

hence f * F = (I --> f) "*" F by Th1; :: thesis: verum