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

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