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 = F "*" (I --> 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 = F "*" (I --> f)
let f be Morphism of C; :: thesis: for F being Function of I, the carrier' of C holds F * f = F "*" (I --> f)
let F be Function of I, the carrier' of C; :: thesis: F * f = F "*" (I --> f)

now :: thesis: for x being set st x in I holds
(F * f) /. x = (F "*" (I --> f)) /. x

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

end;

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