let A, B be non empty reflexive AltGraph ; :: thesis: for F being feasible Contravariant FunctorStr over 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 over 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 30 :: 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 )
( 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 2, ZFMISC_1:def 2;
then A3: Morph-Map (F,a,b) is one-to-one by A1;
A4: <^(F . b),(F . a)^> <> {} by A2, FUNCTOR0:def 19;
then ( F . f = (Morph-Map (F,a,b)) . f & F . g = (Morph-Map (F,a,b)) . g ) by A2, FUNCTOR0:def 16;
hence ( F . f = F . g implies f = g ) by A2, A4, A3, FUNCT_2:19; :: thesis: verum