let C1, C2 be non empty AltGraph ; 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; ( <^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^> <> {}
; 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; for o1 being Object of C1 holds (C1 --> m) . o1 = o2
let o1 be Object of C1; (C1 --> m) . o1 = o2
A2:
[o1,o1] in [: the carrier of C1, the carrier of C1:]
by ZFMISC_1:87;
thus (C1 --> m) . o1 =
(([: the carrier of C1, the carrier of C1:] --> [o2,o2]) . (o1,o1)) `1
by A1, Def17
.=
[o2,o2] `1
by A2, FUNCOP_1:7
.=
o2
; verum