let A be non empty AltGraph ; 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; ( <^o1,o2^> <> {} implies for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m )
assume
<^o1,o2^> <> {}
; for m being Morphism of o1,o2 holds (Morph-Map ((id A),o1,o2)) . m = m
let m be Morphism of o1,o2; (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
;
verum