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 A1: <^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
A2: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:106;
Morph-Map ((id A),o1,o2) = (id the Arrows of A) . [o1,o2] by Def30;
hence (Morph-Map ((id A),o1,o2)) . m = (id ( the Arrows of A . (o1,o2))) . m by A2, MSUALG_3:def 1
.= (id <^o1,o2^>) . m by ALTCAT_1:def 2
.= m by A1, FUNCT_1:35 ;
:: thesis: verum