let A be non empty AltGraph ; :: thesis: for o1, o2 being object of A st <^o1,o2^> <> {} holds
for F being feasible Covariant FunctorStr of 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 of 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 of A,A st F = id A holds
for m being Morphism of o1,o2 holds F . m = m
let F be feasible Covariant FunctorStr of 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, Def19;
hence F . m = (Morph-Map F,o1,o2) . m by A1, Def16
.= m by A1, A2, Th31 ;
:: thesis: verum