let C1 be non empty AltGraph ; :: thesis: for C2 being non empty reflexive AltGraph
for o2 being object of
for m being Morphism of ,
for o, o' being object of
for f being Morphism of , st <^o,o'^> <> {} holds
(C1 --> m) . f = m
let C2 be non empty reflexive AltGraph ; :: thesis: for o2 being object of
for m being Morphism of ,
for o, o' being object of
for f being Morphism of , st <^o,o'^> <> {} holds
(C1 --> m) . f = m
let o2 be object of ; :: thesis: for m being Morphism of ,
for o, o' being object of
for f being Morphism of , st <^o,o'^> <> {} holds
(C1 --> m) . f = m
A1: <^o2,o2^> <> {} by ALTCAT_2:def 7;
let m be Morphism of ,; :: thesis: for o, o' being object of
for f being Morphism of , st <^o,o'^> <> {} holds
(C1 --> m) . f = m
set F = C1 --> m;
let o, o' be object of ; :: thesis: for f being Morphism of , st <^o,o'^> <> {} holds
(C1 --> m) . f = m
let f be Morphism of ,; :: thesis: ( <^o,o'^> <> {} implies (C1 --> m) . f = m )
assume A2: <^o,o'^> <> {} ; :: thesis: (C1 --> m) . f = m
then <^((C1 --> m) . o'),((C1 --> m) . o)^> <> {} by Def20;
hence (C1 --> m) . f = (Morph-Map (C1 --> m),o,o') . f by A2, Def17
.= m by A1, A2, Th25 ;
:: thesis: verum