let C1, C2 be non empty AltCatStr ; :: thesis: for F being Contravariant FunctorStr over C1,C2
for o1, o2 being Object of C1
for Fm being Morphism of (F . o2),(F . o1) st <^o1,o2^> <> {} & F is full & F is feasible holds
ex m being Morphism of o1,o2 st Fm = F . m
let F be Contravariant FunctorStr over C1,C2; :: thesis: for o1, o2 being Object of C1
for Fm being Morphism of (F . o2),(F . o1) st <^o1,o2^> <> {} & F is full & F is feasible holds
ex m being Morphism of o1,o2 st Fm = F . m
let o1, o2 be Object of C1; :: thesis: for Fm being Morphism of (F . o2),(F . o1) st <^o1,o2^> <> {} & F is full & F is feasible holds
ex m being Morphism of o1,o2 st Fm = F . m
let Fm be Morphism of (F . o2),(F . o1); :: thesis: ( <^o1,o2^> <> {} & F is full & F is feasible implies ex m being Morphism of o1,o2 st Fm = F . m )
assume A1: <^o1,o2^> <> {} ; :: thesis: ( not F is full or not F is feasible or ex m being Morphism of o1,o2 st Fm = F . m )
assume F is full ; :: thesis: ( not F is feasible or ex m being Morphism of o1,o2 st Fm = F . m )
then Morph-Map (F,o1,o2) is onto by Th14;
then A2: rng (Morph-Map (F,o1,o2)) = <^(F . o2),(F . o1)^> ;
assume F is feasible ; :: thesis: ex m being Morphism of o1,o2 st Fm = F . m
then A3: <^(F . o2),(F . o1)^> <> {} by A1;
then consider m being object such that
A4: m in dom (Morph-Map (F,o1,o2)) and
A5: Fm = (Morph-Map (F,o1,o2)) . m by A2, FUNCT_1:def 3;
reconsider m = m as Morphism of o1,o2 by A3, A4, FUNCT_2:def 1;
take m ; :: thesis: Fm = F . m
thus Fm = F . m by A1, A3, A5, FUNCTOR0:def 16; :: thesis: verum