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