let A be non empty AltGraph ; :: thesis: for o1, o2 being Object of A st <^o1,o2^> <> {} holds
for F being feasible Covariant FunctorStr over A,A st F = id A holds
for m being Morphism of o1,o2 holds F . m = m
let o1, o2 be Object of A; :: thesis: ( <^o1,o2^> <> {} implies for F being feasible Covariant FunctorStr over A,A st F = id A holds
for m being Morphism of o1,o2 holds F . m = m )
assume A1: <^o1,o2^> <> {} ; :: thesis: for F being feasible Covariant FunctorStr over A,A st F = id A holds
for m being Morphism of o1,o2 holds F . m = m
let F be feasible Covariant FunctorStr over A,A; :: thesis: ( F = id A implies for m being Morphism of o1,o2 holds F . m = m )
assume A2: F = id A ; :: thesis: for m being Morphism of o1,o2 holds F . m = m
let m be Morphism of o1,o2; :: thesis: F . m = m
<^(F . o1),(F . o2)^> <> {} by A1, Def18;
hence F . m = (Morph-Map (F,o1,o2)) . m by A1, Def15
.= m by A1, A2, Th30 ;
:: thesis: verum