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
A9: for f being Morphism of C holds F1 . f = [[((I `1 ) . (dom f)),((I `1 ) . (cod f))],((I `2 ) . f)] and
A10: for f being Morphism of C holds F2 . f = [[((I `1 ) . (dom f)),((I `1 ) . (cod f))],((I `2 ) . f)] ; :: thesis: F1 = F2

now

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 A9
.= F2 . f by A10 ; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:113; :: thesis: verum