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

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