let A, B be non empty AltGraph ; :: thesis: for F being Contravariant FunctorStr of 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 of 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 33,FUNCTOR0:def 35 :: 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 8,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 )
A3: dom the ObjectMap of F = [:the carrier of A,the carrier of A:] by FUNCT_2:def 1;
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 A4: <^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 )
[a,b] in rng the ObjectMap of F by A2, ZFMISC_1:def 2;
then consider x being set such that
A5: ( x in [:the carrier of A,the carrier of A:] & [a,b] = the ObjectMap of F . x ) by A3, FUNCT_1:def 5;
consider d, c being set such that
A6: ( d in the carrier of A & c in the carrier of A & [d,c] = x ) by A5, ZFMISC_1:def 2;
reconsider c = c, d = d as object of A by A6;
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 )
the ObjectMap of F is Contravariant by FUNCTOR0:def 14;
then consider g being Function of the carrier of A,the carrier of B such that
A7: the ObjectMap of F = ~ [:g,g:] by FUNCTOR0:def 3;
A8: ( dom the ObjectMap of F = [:the carrier of A,the carrier of A:] & [c,c] in [:the carrier of A,the carrier of A:] & [d,c] in [:the carrier of A,the carrier of A:] & [d,d] in [:the carrier of A,the carrier of A:] ) by FUNCT_2:def 1, ZFMISC_1:def 2;
then ( the ObjectMap of F . c,c = [:g,g:] . c,c & the ObjectMap of F . d,d = [:g,g:] . d,d ) by A7, FUNCT_4:44;
then ( the ObjectMap of F . c,c = [(g . c),(g . c)] & the ObjectMap of F . d,d = [(g . d),(g . d)] ) by FUNCT_3:96;
then A9: ( F . c = g . c & F . d = g . d ) by MCART_1:7;
A10: the ObjectMap of F . d,c = [:g,g:] . c,d by A7, A8, FUNCT_4:44
.= [(F . c),(F . d)] by A9, FUNCT_3:96 ;
rng (Morph-Map F,d,c) = (the Arrows of B * the ObjectMap of F) . [d,c] by A1, A5, A6, MSUALG_3:def 3
.= <^a,b^> by A5, A6, FUNCT_2:21 ;
then consider g being set such that
A11: ( g in dom (Morph-Map F,d,c) & f = (Morph-Map F,d,c) . g ) by A4, FUNCT_1:def 5;
reconsider g = g as Morphism of d,c by A11;
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, A6, A10, A11, ZFMISC_1:33; :: thesis: f = F . g
thus f = F . g by A4, A5, A6, A10, A11, FUNCTOR0:def 17; :: thesis: verum