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 :: thesis: for fg being Morphism of [:A,B:] holds F1 . fg = F2 . fg

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:27;
A3: ( dom (id (cod f)) = cod f & dom g = cod (id (dom g)) ) ;
A4: fg = [((id (cod f)) (*) f),g] by A2, Th3
.= [((id (cod f)) (*) f),(g (*) (id (dom g)))] by Th4
.= [(id (cod f)),g] (*) [f,(id (dom g))] by A3, CAT_2:29 ;
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 XTUPLE_0:1;
then A7: F1 ?- (dom f) = F2 ?- (dom f) by XTUPLE_0:1;
A8: F1 ?- (cod f) = F2 ?- (cod f) by A6, XTUPLE_0:1;
then A9: F1 . ((id (cod f)),g) = (F2 ?- (cod f)) . g by CAT_2:36
.= F2 . ((id (cod f)),g) by CAT_2:36 ;
A10: cod [f,(id (dom g))] = [(cod f),(cod (id (dom g)))] by CAT_2:28
.= [(cod f),(dom g)]
.= [(dom (id (cod f))),(dom g)]
.= dom [(id (cod f)),g] by CAT_2:28 ;
F1 . (f,(id (dom g))) = (F1 ?- f) . (dom g) by Th15
.= (F2 ?- f) . (dom g) by A5, A7, A8, XTUPLE_0:1
.= F2 . (f,(id (dom g))) by Th15 ;
hence F1 . fg = (F2 . [(id (cod f)),g]) (*) (F2 . [f,(id (dom g))]) by A4, A9, A10, CAT_1:64
.= F2 . fg by A4, A10, CAT_1:64 ;
:: thesis: verum

end;

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