let A, B be non empty reflexive AltGraph ; :: thesis: for F being feasible Contravariant FunctorStr of A,B st F is faithful holds
for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F . f = F . g holds
f = g
let F be feasible Contravariant FunctorStr of A,B; :: thesis: ( F is faithful implies for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F . f = F . g holds
f = g )
assume A1: for i being set
for f being Function st i in dom the MorphMap of F & the MorphMap of F . i = f holds
f is one-to-one ; :: according to MSUALG_3:def 2,FUNCTOR0:def 31 :: thesis: for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F . f = F . g holds
f = g
let a, b be object of A; :: thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st F . f = F . g holds
f = g )
assume A2: <^a,b^> <> {} ; :: thesis: for f, g being Morphism of a,b st F . f = F . g holds
f = g
let f, g be Morphism of a,b; :: thesis: ( F . f = F . g implies f = g )
A3: <^(F . b),(F . a)^> <> {} by A2, FUNCTOR0:def 20;
then A4: ( F . f = (Morph-Map F,a,b) . f & F . g = (Morph-Map F,a,b) . g ) by A2, FUNCTOR0:def 17;
( dom the MorphMap of F = [:the carrier of A,the carrier of A:] & [a,b] in [:the carrier of A,the carrier of A:] ) by PARTFUN1:def 4, ZFMISC_1:def 2;
then ( Morph-Map F,a,b is one-to-one & f in <^a,b^> & g in <^a,b^> ) by A1, A2;
hence ( F . f = F . g implies f = g ) by A3, A4, FUNCT_2:25; :: thesis: verum