let C1, C2 be non empty AltGraph ; :: thesis: for o2 being object of C2 st <^o2,o2^> <> {} holds
for m being Morphism of o2,o2
for o1 being object of C1 holds (C1 --> m) . o1 = o2
let o2 be object of C2; :: thesis: ( <^o2,o2^> <> {} implies for m being Morphism of o2,o2
for o1 being object of C1 holds (C1 --> m) . o1 = o2 )
assume A1: <^o2,o2^> <> {} ; :: thesis: for m being Morphism of o2,o2
for o1 being object of C1 holds (C1 --> m) . o1 = o2
let m be Morphism of o2,o2; :: thesis: for o1 being object of C1 holds (C1 --> m) . o1 = o2
let o1 be object of C1; :: thesis: (C1 --> m) . o1 = o2
A2: [o1,o1] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:106;
thus (C1 --> m) . o1 = (([:the carrier of C1,the carrier of C1:] --> [o2,o2]) . o1,o1) `1 by A1, Def18
.= [o2,o2] `1 by A2, FUNCOP_1:13
.= o2 by MCART_1:7 ; :: thesis: verum