let A, B, C be Category; :: thesis: for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let F1, G1 be Functor of A,B; :: thesis: for F2, G2 being Functor of A,C st F1 is_transformable_to G1 & F2 is_transformable_to G2 holds
for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let F2, G2 be Functor of A,C; :: thesis: ( F1 is_transformable_to G1 & F2 is_transformable_to G2 implies for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)] )
assume that
A1: F1 is_transformable_to G1 and
A2: F2 is_transformable_to G2 ; :: thesis: for t1 being transformation of F1,G1
for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let t1 be transformation of F1,G1; :: thesis: for t2 being transformation of F2,G2
for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let t2 be transformation of F2,G2; :: thesis: for a being Object of A holds <:t1,t2:> . a = [(t1 . a),(t2 . a)]
let a be Object of A; :: thesis: <:t1,t2:> . a = [(t1 . a),(t2 . a)]
reconsider s1 = t1 as Function of the carrier of A, the carrier' of B ;
reconsider s2 = t2 as Function of the carrier of A, the carrier' of C ;
thus <:t1,t2:> . a = [(s1 . a),(s2 . a)] by FUNCT_3:59
.= [(t1 . a),(s2 . a)] by A1, NATTRA_1:def 5
.= [(t1 . a),(t2 . a)] by A2, NATTRA_1:def 5 ; :: thesis: verum