let A, B, C be Category; :: thesis: for F being Functor of A,B
for G being Functor of A,C
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds <:F,G:> . f = [(F . f),(G . f)]
let F be Functor of A,B; :: thesis: for G being Functor of A,C
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds <:F,G:> . f = [(F . f),(G . f)]
let G be Functor of A,C; :: thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds <:F,G:> . f = [(F . f),(G . f)]
let a, b be Object of A; :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds <:F,G:> . f = [(F . f),(G . f)] )
assume A1: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b holds <:F,G:> . f = [(F . f),(G . f)]
let f be Morphism of a,b; :: thesis: <:F,G:> . f = [(F . f),(G . f)]
reconsider g = f as Morphism of A ;
thus <:F,G:> . f = <:F,G:> . g by A1, NATTRA_1:def 1
.= [(F . g),(G . g)] by FUNCT_3:59
.= [(F . g),(G . f)] by A1, NATTRA_1:def 1
.= [(F . f),(G . f)] by A1, NATTRA_1:def 1 ; :: thesis: verum