let C1 be non empty AltGraph ; :: thesis: for C2 being non empty reflexive AltGraph
for o2 being Object of C2
for m being Morphism of o2,o2
for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds
for o, o9 being Object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m
let C2 be non empty reflexive AltGraph ; :: thesis: for o2 being Object of C2
for m being Morphism of o2,o2
for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds
for o, o9 being Object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m
let o2 be Object of C2; :: thesis: for m being Morphism of o2,o2
for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds
for o, o9 being Object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m
A1: <^o2,o2^> <> {} by ALTCAT_2:def 7;
let m be Morphism of o2,o2; :: thesis: for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds
for o, o9 being Object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m
let F be feasible Covariant FunctorStr over C1,C2; :: thesis: ( F = C1 --> m implies for o, o9 being Object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m )
assume A2: F = C1 --> m ; :: thesis: for o, o9 being Object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m
let o, o9 be Object of C1; :: thesis: for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m
let f be Morphism of o,o9; :: thesis: ( <^o,o9^> <> {} implies F . f = m )
assume A3: <^o,o9^> <> {} ; :: thesis: F . f = m
then <^(F . o),(F . o9)^> <> {} by Def18;
hence F . f = (Morph-Map (F,o,o9)) . f by A3, Def15
.= m by A1, A2, A3, Th24 ;
:: thesis: verum