let A, B be non empty AltGraph ; :: thesis: for F being Contravariant 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

( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g )

let F be Contravariant 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

( b = F . c & a = 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

( b = F . c & a = 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

( b = F . c & a = 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

( b = F . c & a = 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

( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g )

let f be Morphism of a,b; :: thesis: ex c, d being Object of A ex g being Morphism of c,d st

( b = F . c & a = 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 A2, FUNCT_2:def 1, ZFMISC_1:def 2;

then consider x being object such that

A4: x in [: the carrier of A, the carrier of A:] and

A5: [a,b] = the ObjectMap of F . x by FUNCT_1:def 3;

A6: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def 1;

the ObjectMap of F is Contravariant by FUNCTOR0:def 13;

then consider g being Function of the carrier of A, the carrier of B such that

A7: the ObjectMap of F = ~ [:g,g:] ;

consider d, c being object such that

A8: ( d in the carrier of A & c in the carrier of A ) and

A9: [d,c] = x by A4, ZFMISC_1:def 2;

reconsider c = c, d = d as Object of A by A8;

[c,c] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

then the ObjectMap of F . (c,c) = [:g,g:] . (c,c) by A7, A6, FUNCT_4:43;

then the ObjectMap of F . (c,c) = [(g . c),(g . c)] by FUNCT_3:75;

then A10: F . c = g . c ;

[d,d] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

then the ObjectMap of F . (d,d) = [:g,g:] . (d,d) by A7, A6, FUNCT_4:43;

then the ObjectMap of F . (d,d) = [(g . d),(g . d)] by FUNCT_3:75;

then A11: F . d = g . d ;

[d,c] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

then A12: the ObjectMap of F . (d,c) = [:g,g:] . (c,d) by A7, A6, FUNCT_4:43

.= [(F . c),(F . d)] by A10, A11, FUNCT_3:75 ;

rng (Morph-Map (F,d,c)) = ( the Arrows of B * the ObjectMap of F) . [d,c] by A1, A4, A9

.= <^a,b^> by A4, A5, A9, FUNCT_2:15 ;

then consider g being object such that

A13: g in dom (Morph-Map (F,d,c)) and

A14: f = (Morph-Map (F,d,c)) . g by A3, FUNCT_1:def 3;

take d ; :: thesis: ex d being Object of A ex g being Morphism of d,d st

( b = F . d & a = F . d & <^d,d^> <> {} & f = F . g )

take c ; :: thesis: ex g being Morphism of d,c st

( b = F . d & a = F . c & <^d,c^> <> {} & f = F . g )

reconsider g = g as Morphism of d,c by A13;

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

thus ( b = F . d & a = F . c & <^d,c^> <> {} ) by A5, A9, A12, A13, XTUPLE_0:1; :: thesis: f = F . g

thus f = F . g by A3, A5, A9, A12, A13, A14, FUNCTOR0:def 16; :: thesis: verum

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

( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g )

let F be Contravariant 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

( b = F . c & a = 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

( b = F . c & a = 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

( b = F . c & a = 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

( b = F . c & a = 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

( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g )

let f be Morphism of a,b; :: thesis: ex c, d being Object of A ex g being Morphism of c,d st

( b = F . c & a = 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 A2, FUNCT_2:def 1, ZFMISC_1:def 2;

then consider x being object such that

A4: x in [: the carrier of A, the carrier of A:] and

A5: [a,b] = the ObjectMap of F . x by FUNCT_1:def 3;

A6: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def 1;

the ObjectMap of F is Contravariant by FUNCTOR0:def 13;

then consider g being Function of the carrier of A, the carrier of B such that

A7: the ObjectMap of F = ~ [:g,g:] ;

consider d, c being object such that

A8: ( d in the carrier of A & c in the carrier of A ) and

A9: [d,c] = x by A4, ZFMISC_1:def 2;

reconsider c = c, d = d as Object of A by A8;

[c,c] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

then the ObjectMap of F . (c,c) = [:g,g:] . (c,c) by A7, A6, FUNCT_4:43;

then the ObjectMap of F . (c,c) = [(g . c),(g . c)] by FUNCT_3:75;

then A10: F . c = g . c ;

[d,d] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

then the ObjectMap of F . (d,d) = [:g,g:] . (d,d) by A7, A6, FUNCT_4:43;

then the ObjectMap of F . (d,d) = [(g . d),(g . d)] by FUNCT_3:75;

then A11: F . d = g . d ;

[d,c] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;

then A12: the ObjectMap of F . (d,c) = [:g,g:] . (c,d) by A7, A6, FUNCT_4:43

.= [(F . c),(F . d)] by A10, A11, FUNCT_3:75 ;

rng (Morph-Map (F,d,c)) = ( the Arrows of B * the ObjectMap of F) . [d,c] by A1, A4, A9

.= <^a,b^> by A4, A5, A9, FUNCT_2:15 ;

then consider g being object such that

A13: g in dom (Morph-Map (F,d,c)) and

A14: f = (Morph-Map (F,d,c)) . g by A3, FUNCT_1:def 3;

take d ; :: thesis: ex d being Object of A ex g being Morphism of d,d st

( b = F . d & a = F . d & <^d,d^> <> {} & f = F . g )

take c ; :: thesis: ex g being Morphism of d,c st

( b = F . d & a = F . c & <^d,c^> <> {} & f = F . g )

reconsider g = g as Morphism of d,c by A13;

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

thus ( b = F . d & a = F . c & <^d,c^> <> {} ) by A5, A9, A12, A13, XTUPLE_0:1; :: thesis: f = F . g

thus f = F . g by A3, A5, A9, A12, A13, A14, FUNCTOR0:def 16; :: thesis: verum