let C1, C2 be non empty AltCatStr ; :: thesis: for F being Contravariant FunctorStr of 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 of 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)^> by FUNCT_2:def 3;
assume F is feasible ; :: thesis: ex m being Morphism of o1,o2 st Fm = F . m
then A3: <^(F . o2),(F . o1)^> <> {} by A1, FUNCTOR0:def 20;
then consider m being set 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 5;
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 17; :: thesis: verum