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 :: thesis: for x being set st x in I holds
(f * F) /. x = ((I --> f) "*" F) /. x

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 Def6
.= ((I --> f) /. x) (*) (F /. x) by A1, Th2
.= ((I --> f) "*" F) /. x by A1, Def7 ;
:: thesis: verum

end;

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