let A, B be non empty AltGraph ; :: thesis: for F being Covariant FunctorStr over A,B st F is surjective holds
for a, b being Object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being Object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )

let F be Covariant FunctorStr over A,B; :: thesis: ( F is surjective implies for a, b being Object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being Object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g ) )

given f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that A1: ( f = the MorphMap of F & f is "onto" ) ; :: according to FUNCTOR0:def 32,FUNCTOR0:def 34 :: thesis: ( not F is onto or for a, b being Object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being Object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g ) )

assume A2: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] ; :: according to FUNCTOR0:def 7,FUNCT_2:def 3 :: thesis: for a, b being Object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being Object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )

let a, b be Object of B; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being Object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g ) )

assume A3: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b ex c, d being Object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )

the ObjectMap of F is Covariant by FUNCTOR0:def 12;
then consider g being Function of the carrier of A, the carrier of B such that
A4: the ObjectMap of F = [:g,g:] ;
let f be Morphism of a,b; :: thesis: ex c, d being Object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )

( dom the ObjectMap of F = [: the carrier of A, the carrier of A:] & [a,b] in rng the ObjectMap of F ) by ;
then consider x being object such that
A5: x in [: the carrier of A, the carrier of A:] and
A6: [a,b] = the ObjectMap of F . x by FUNCT_1:def 3;
consider c, d being object such that
A7: ( c in the carrier of A & d in the carrier of A ) and
A8: [c,d] = x by ;
reconsider c = c, d = d as Object of A by A7;
the ObjectMap of F . (d,d) = [(g . d),(g . d)] by ;
then A9: F . d = g . d ;
the ObjectMap of F . (c,c) = [(g . c),(g . c)] by ;
then F . c = g . c ;
then A10: the ObjectMap of F . (c,d) = [(F . c),(F . d)] by ;
rng (Morph-Map (F,c,d)) = ( the Arrows of B * the ObjectMap of F) . [c,d] by A1, A5, A8
.= <^a,b^> by ;
then consider g being object such that
A11: g in dom (Morph-Map (F,c,d)) and
A12: f = (Morph-Map (F,c,d)) . g by ;
take c ; :: thesis: ex d being Object of A ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )

take d ; :: thesis: ex g being Morphism of c,d st
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )

reconsider g = g as Morphism of c,d by A11;
take g ; :: thesis: ( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )
thus ( a = F . c & b = F . d & <^c,d^> <> {} ) by ; :: thesis: f = F . g
thus f = F . g by ; :: thesis: verum