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 :: thesis: for m being Morphism of B holds F1 . m = F2 . m

let m be Morphism of B; :: thesis: F1 . m = F2 . m
Hom ((F1 . (dom m)),(F2 . (dom m))) <> {} by A1;
then A2: F1 . (dom m) = F2 . (dom m) by Def17;
A3: m in Hom ((dom m),(cod m)) ;
then Hom ((F1 . (dom m)),(F1 . (cod m))) <> {} by CAT_1:81;
then F1 . (dom m) = F1 . (cod m) by Def17;
then A4: Hom ((F1 . (dom m)),(F1 . (cod m))) = {(id (F1 . (dom m)))} by Th33;
Hom ((F2 . (dom m)),(F2 . (cod m))) <> {} by A3, CAT_1:81;
then F2 . (dom m) = F2 . (cod m) by Def17;
then A5: Hom ((F2 . (dom m)),(F2 . (cod m))) = {(id (F2 . (dom m)))} by Th33;
F1 . m in Hom ((F1 . (dom m)),(F1 . (cod m))) by A3, CAT_1:81;
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:81;
hence F1 . m = F2 . m by A2, A6, A5, TARSKI:def 1; :: thesis: verum

end;

hence F1 = F2 ; :: thesis: verum