let F1, F2 be Functor of C,T; :: thesis: ( ( for f being Morphism of C holds F1 . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] ) & ( for f being Morphism of C holds F2 . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] ) implies F1 = F2 )
assume that
A12: for f being Morphism of C holds F1 . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] and
A13: for f being Morphism of C holds F2 . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] ; :: thesis: F1 = F2

now :: thesis: for f being Morphism of C holds F1 . f = F2 . f

let f be Morphism of C; :: thesis: F1 . f = F2 . f
thus F1 . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] by A12
.= F2 . f by A13 ; :: thesis: verum

end;

hence F1 = F2 ; :: thesis: verum