let A be non empty AltGraph ; :: thesis: for o1, o2 being Object of A st <^o1,o2^> <> {} holds
for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m
let o1, o2 be Object of A; :: thesis: ( <^o1,o2^> <> {} implies for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m )
assume <^o1,o2^> <> {} ; :: thesis: for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m
let m be Morphism of o1,o2; :: thesis: (Morph-Map ((id A),o1,o2)) . m = m
A1: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87;
Morph-Map ((id A),o1,o2) = (id the Arrows of A) . [o1,o2] by Def29;
hence (Morph-Map ((id A),o1,o2)) . m = (id ( the Arrows of A . (o1,o2))) . m by A1, MSUALG_3:def 1
.= (id <^o1,o2^>) . m by ALTCAT_1:def 1
.= m ;
:: thesis: verum