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)

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

hence
F * f = F "*" (I --> f)
by Th1; :: thesis: verum(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;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