let A, B be non empty reflexive AltGraph ; :: thesis: for F being feasible Covariant 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 Covariant 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 ;
then A3: Morph-Map (F,a,b) is one-to-one by A1;
A4: <^(F . a),(F . b)^> <> {} by ;
then ( F . f = (Morph-Map (F,a,b)) . f & F . g = (Morph-Map (F,a,b)) . g ) by ;
hence ( F . f = F . g implies f = g ) by ; :: thesis: verum