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
A2: m in Hom (dom m),(cod m) ;
Hom (F1 . (dom m)),(F2 . (dom m)) <> {} by A1, Def2;
then A3: F1 . (dom m) = F2 . (dom m) by Th45;
A4: F1 . m in Hom (F1 . (dom m)),(F1 . (cod m)) by A2, CAT_1:123;
Hom (F1 . (dom m)),(F1 . (cod m)) <> {} by A2, CAT_1:123;
then F1 . (dom m) = F1 . (cod m) by Th45;
then Hom (F1 . (dom m)),(F1 . (cod m)) = {(id (F1 . (dom m)))} by Th44;
then A5: F1 . m = id (F1 . (dom m)) by A4, TARSKI:def 1;
A6: F2 . m in Hom (F2 . (dom m)),(F2 . (cod m)) by A2, CAT_1:123;
Hom (F2 . (dom m)),(F2 . (cod m)) <> {} by A2, CAT_1:123;
then F2 . (dom m) = F2 . (cod m) by Th45;
then Hom (F2 . (dom m)),(F2 . (cod m)) = {(id (F2 . (dom m)))} by Th44;
hence F1 . m = F2 . m by A3, A5, A6, TARSKI:def 1; :: thesis: verum

end;

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