let A, B, C be Category; :: thesis: for F1, F2 being Functor of [:A,B:],C st export F1 = export F2 holds
F1 = F2
let F1, F2 be Functor of [:A,B:],C; :: thesis: ( export F1 = export F2 implies F1 = F2 )
assume A1: export F1 = export F2 ; :: thesis: F1 = F2

now

let fg be Morphism of [:A,B:]; :: thesis: F1 . fg = F2 . fg
consider f being Morphism of A, g being Morphism of B such that
A2: fg = [f,g] by CAT_2:37;
A3: ( dom (id (cod f)) = cod f & dom g = cod (id (dom g)) ) by CAT_1:44;
A4: fg = [((id (cod f)) * f),g] by A2, Th6
.= [((id (cod f)) * f),(g * (id (dom g)))] by Th7
.= [(id (cod f)),g] * [f,(id (dom g))] by A3, CAT_2:39 ;
A5: [[(F1 ?- (dom f)),(F1 ?- (cod f))],(F1 ?- f)] = (export F2) . f by A1, Def4
.= [[(F2 ?- (dom f)),(F2 ?- (cod f))],(F2 ?- f)] by Def4 ;
then A6: [(F1 ?- (dom f)),(F1 ?- (cod f))] = [(F2 ?- (dom f)),(F2 ?- (cod f))] by ZFMISC_1:33;
then A7: F1 ?- (dom f) = F2 ?- (dom f) by ZFMISC_1:33;
A8: F1 ?- (cod f) = F2 ?- (cod f) by A6, ZFMISC_1:33;
then A9: F1 . ((id (cod f)),g) = (F2 ?- (cod f)) . g by CAT_2:47
.= F2 . ((id (cod f)),g) by CAT_2:47 ;
A10: cod [f,(id (dom g))] = [(cod f),(cod (id (dom g)))] by CAT_2:38
.= [(cod f),(dom g)] by CAT_1:44
.= [(dom (id (cod f))),(dom g)] by CAT_1:44
.= dom [(id (cod f)),g] by CAT_2:38 ;
F1 . (f,(id (dom g))) = (F1 ?- f) . (dom g) by Th19
.= (F2 ?- f) . (dom g) by A5, A7, A8, ZFMISC_1:33
.= F2 . (f,(id (dom g))) by Th19 ;
hence F1 . fg = (F2 . [(id (cod f)),g]) * (F2 . [f,(id (dom g))]) by A4, A9, A10, CAT_1:99
.= F2 . fg by A4, A10, CAT_1:99 ;
:: thesis: verum

end;

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