let A be discrete Category; :: thesis: for B being Category
for F1, F2 being Functor of B,A st F1 is_transformable_to F2 holds
F1 = F2
let B be Category; :: thesis: for F1, F2 being Functor of B,A st F1 is_transformable_to F2 holds
F1 = F2
let F1, F2 be Functor of B,A; :: thesis: ( F1 is_transformable_to F2 implies F1 = F2 )
assume A1: F1 is_transformable_to F2 ; :: thesis: F1 = F2

now

let m be Morphism of B; :: thesis: F1 . m = F2 . m
Hom (F1 . (dom m)),(F2 . (dom m)) <> {} by A1, Def2;
then A2: F1 . (dom m) = F2 . (dom m) by Th45;
A3: m in Hom (dom m),(cod m) ;
then Hom (F1 . (dom m)),(F1 . (cod m)) <> {} by CAT_1:123;
then F1 . (dom m) = F1 . (cod m) by Th45;
then A4: Hom (F1 . (dom m)),(F1 . (cod m)) = {(id (F1 . (dom m)))} by Th44;
Hom (F2 . (dom m)),(F2 . (cod m)) <> {} by A3, CAT_1:123;
then F2 . (dom m) = F2 . (cod m) by Th45;
then A5: Hom (F2 . (dom m)),(F2 . (cod m)) = {(id (F2 . (dom m)))} by Th44;
F1 . m in Hom (F1 . (dom m)),(F1 . (cod m)) by A3, CAT_1:123;
then A6: F1 . m = id (F1 . (dom m)) by A4, TARSKI:def 1;
F2 . m in Hom (F2 . (dom m)),(F2 . (cod m)) by A3, CAT_1:123;
hence F1 . m = F2 . m by A2, A6, A5, TARSKI:def 1; :: thesis: verum

end;

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