let C be non empty AltCatStr ; :: thesis: for a, b, f being set st f in the Arrows of C . (a,b) holds
ex o1, o2 being object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
let a, b, f be set ; :: thesis: ( f in the Arrows of C . (a,b) implies ex o1, o2 being object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 ) )
assume A1: f in the Arrows of C . (a,b) ; :: thesis: ex o1, o2 being object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
then [a,b] in dom the Arrows of C by FUNCT_1:def 2;
then [a,b] in [: the carrier of C, the carrier of C:] by PARTFUN1:def 2;
then reconsider o1 = a, o2 = b as object of C by ZFMISC_1:87;
take o1 ; :: thesis: ex o2 being object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
take o2 ; :: thesis: ( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )
thus ( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 ) by A1, ALTCAT_1:def 1; :: thesis: verum