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

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

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